Home

Dependencies

Click a node to copy its name

addSubgroupIndependenceNumber_ge_card_of_independent

Theorem 21

LaTeX Lean

addSubgroupIndependenceNumber_le_independenceNumber

Theorem 22

LaTeX Lean

addSubgroupShannonCapacity_ge_root

Theorem 24

LaTeX Lean

addSubgroupShannonCapacity_le_shannonCapacity

Theorem 23

LaTeX Lean

addSubgroupShannonCapacity_lift

Theorem 53

LaTeX Lean

addSubgroupShannonCapacity_mono_of_addHom_cohom

Theorem 25

LaTeX Lean

Construction.a

Definition 135

LaTeX Lean

Construction.a_mod_denom

Theorem 139

LaTeX Lean

Construction.A_Rα_form

Theorem 178

LaTeX Lean

Construction.A_Rα_form_nat

Theorem 177

LaTeX Lean

Construction.AB_eq_pI

Theorem 187

LaTeX Lean

Construction.AB_eq_pI_nat

Theorem 185

LaTeX Lean

Construction.AB_eq_pI_real

Theorem 180

LaTeX Lean

Construction.alpha_in_range

Theorem 155

LaTeX Lean

Construction.alpha_real_in_range

Theorem 164

LaTeX Lean

Construction.aReal

Definition 136

LaTeX Lean

Construction.B_Rα_form

Theorem 179

LaTeX Lean

Construction.B_Rα_form_nat

Theorem 175

LaTeX Lean

Construction.denom_ne_zero

Theorem 141

LaTeX Lean

Construction.denom_ne_zero_nat

Theorem 182

LaTeX Lean

Construction.denom_pos

Theorem 140

LaTeX Lean

Construction.denom_pos_nat

Theorem 181

LaTeX Lean

Construction.det_B_eq_p

Theorem 190

LaTeX Lean

Construction.det_B_eq_p_nat

Theorem 189

LaTeX Lean

Construction.det_ratio_eq_p_real

Theorem 188

LaTeX Lean

Construction.diagPow

Definition 156

LaTeX Lean

Construction.diagPow_eq_Dα

Theorem 173

LaTeX Lean

Construction.factorization_lower_eq

Theorem 158

LaTeX Lean

Construction.factorization_upper_eq

Theorem 157

LaTeX Lean

Construction.matrixA

Definition 168

LaTeX Lean

Construction.matrixA_eq_X_add_qI

Theorem 171

LaTeX Lean

Construction.matrixB

Definition 169

LaTeX Lean

Construction.matrixX

Definition 149

LaTeX Lean

Construction.matrixX_real

Definition 152

LaTeX Lean

Construction.matrixX_real_continuous_s

Theorem 154

LaTeX Lean

Construction.matrixX_real_eq_map

Theorem 153

LaTeX Lean

Construction.matrixX_real_isP0_s_pos

Theorem 165

LaTeX Lean

Construction.matrixY

Definition 150

LaTeX Lean

Construction.minDist_A_ge_q

Theorem 172

LaTeX Lean

Construction.numer_ne_zero_nat

Theorem 184

LaTeX Lean

Construction.numer_pos_nat

Theorem 183

LaTeX Lean

Construction.p

Definition 137

LaTeX Lean

Construction.p_numer_div_denom

Theorem 142

LaTeX Lean

Construction.p_over_q_le_a_over_b

Theorem 146

LaTeX Lean

Construction.p_q_are_integers

Theorem 144

LaTeX Lean

Construction.pb_eq_qa_minus

Theorem 145

LaTeX Lean

Construction.Polynomial.eq_zero_of_eval_nat_ge_one

Theorem 186

LaTeX Lean

Construction.q

Definition 138

LaTeX Lean

Construction.q_numer_div_denom

Theorem 143

LaTeX Lean

Construction.q_pos

Theorem 170

LaTeX Lean

Construction.R_sub_bI_isUnit

Theorem 174

LaTeX Lean

Construction.sR_sub_aI_isUnit

Theorem 176

LaTeX Lean

Construction.X_entry

Definition 147

LaTeX Lean

Construction.X_entry_real

Definition 151

LaTeX Lean

Construction.X_factorization

Theorem 159

LaTeX Lean

Construction.X_isP0

Theorem 167

LaTeX Lean

Construction.X_isP0_s_ne_zero

Theorem 163

LaTeX Lean

Construction.X_isP0_s_zero

Theorem 166

LaTeX Lean

Construction.Y_entry

Definition 148

LaTeX Lean

Construction.Y_factorization

Theorem 162

LaTeX Lean

Construction.Y_factorization_lower_eq

Theorem 161

LaTeX Lean

Construction.Y_factorization_upper_eq

Theorem 160

LaTeX Lean

cycleGraph_iso_fractionGraph_two

Definition 41

LaTeX Lean

distMod

Definition 2

LaTeX Lean

distMod_add_left

Theorem 42

LaTeX Lean

distMod_comm

Theorem 4

LaTeX Lean

distMod_eq_one_iff

Theorem 36

LaTeX Lean

distMod_eq_valMinAbs_natAbs

Theorem 3

LaTeX Lean

div_add_one_le_of_rem_pos

Theorem 32

LaTeX Lean

div_sub_le

Theorem 30

LaTeX Lean

fin_sub_eq_one_of_zmod_sub_eq_one

Theorem 39

LaTeX Lean

fin_sub_val_eq_zmod_sub_val

Theorem 38

LaTeX Lean

finEquivZMod

Definition 35

LaTeX Lean

fractionGraph

Definition 5

LaTeX Lean

fractionGraph_adj_add_left

Theorem 43

LaTeX Lean

fractionGraph_cohomomorphism

Theorem 34

LaTeX Lean

fractionGraph_scalarMulMap

Definition 50

LaTeX Lean

fractionGraph_scalarMulMap_injective

Theorem 51

LaTeX Lean

fractionGraph_scalarMulMap_isCohom

Theorem 52

LaTeX Lean

fractionGraph_scalingMap

Definition 29

LaTeX Lean

fractionGraph_scalingMap_isCohom

Theorem 33

LaTeX Lean

fractionGraph_two_eq_circulant

Theorem 37

LaTeX Lean

independenceNumber_ge_card_of_independent

Theorem 16

LaTeX Lean

independenceNumber_ge_natCard_of_independent

Theorem 17

LaTeX Lean

independenceNumber_iso

Theorem 9

LaTeX Lean

independenceNumber_le_card

Theorem 18

LaTeX Lean

independenceNumber_le_of_clique_cover

Theorem 26

LaTeX Lean

independenceNumber_le_of_cohomomorphism

Theorem 6

LaTeX Lean

independenceNumber_strongPower_fractionGraph_le

Theorem 46

LaTeX Lean

indepNum_le_of_iso

Theorem 8

LaTeX Lean

isClique_arc

Theorem 45

LaTeX Lean

isClique_range_fractionGraph

Theorem 44

LaTeX Lean

iso_is_cohomomorphism

Theorem 7

LaTeX Lean

Lattice.abs_canonicalRep_le

Theorem 64

LaTeX Lean

Lattice.canonicalRep

Definition 61

LaTeX Lean

Lattice.canonicalRep_coe

Theorem 63

LaTeX Lean

Lattice.canonicalRepVec

Definition 65

LaTeX Lean

Lattice.card_latticeQuotient_eq

Theorem 81

LaTeX Lean

Lattice.card_latticeQuotient_eq_relIndex

Theorem 80

LaTeX Lean

Lattice.det_mul_eq_pow_of_mul_eq_smul

Theorem 69

LaTeX Lean

Lattice.distMod_eq_abs_canonicalRep

Theorem 62

LaTeX Lean

Lattice.distMod_eq_canonicalRep_diff

Theorem 66

LaTeX Lean

Lattice.exampleA

Definition 83

LaTeX Lean

Lattice.exampleB

Definition 84

LaTeX Lean

Lattice.exists_canonical_lattice_rep

Theorem 68

LaTeX Lean

Lattice.index_intLatticeOfMatrix

Theorem 78

LaTeX Lean

Lattice.index_pZn

Theorem 76

LaTeX Lean

Lattice.inftyNorm

Definition 55

LaTeX Lean

Lattice.intLatticeOfMatrix

Definition 70

LaTeX Lean

Lattice.intLatticeOfMatrix_toSubmodule

Theorem 77

LaTeX Lean

Lattice.IsPAry

Definition 57

LaTeX Lean

Lattice.latticeOfMatrix

Definition 54

LaTeX Lean

Lattice.latticeOfMatrix_add_pZ

Theorem 67

LaTeX Lean

Lattice.latticeQuotient

Definition 58

LaTeX Lean

Lattice.latticeQuotient_addSubgroup

Theorem 60

LaTeX Lean

Lattice.matrixToIndependentSet

Theorem 82

LaTeX Lean

Lattice.minDistance

Definition 56

LaTeX Lean

Lattice.modPHom

Definition 73

LaTeX Lean

Lattice.modPHom_image_intLattice_carrier

Theorem 79

LaTeX Lean

Lattice.modPHom_ker

Theorem 74

LaTeX Lean

Lattice.modPHom_surjective

Theorem 75

LaTeX Lean

Lattice.pZ_subset_lattice

Theorem 59

LaTeX Lean

Lattice.pZn

Definition 71

LaTeX Lean

Lattice.pZn_le_intLattice

Theorem 72

LaTeX Lean

Main.construction_lower_bound

Theorem 212

LaTeX Lean

Main.lattice_to_independent_set

Theorem 213

LaTeX Lean

Main.limit_cycles

Theorem 209

LaTeX Lean

Main.limit_fraction_graphs

Theorem 210

LaTeX Lean

Main.monotonicity

Theorem 215

LaTeX Lean

Main.subgroup_limit

Theorem 211

LaTeX Lean

Main.upper_bound

Theorem 214

LaTeX Lean

MainProofs.a_pos_rat

Theorem 194

LaTeX Lean

MainProofs.AB_eq_pI_int

Theorem 197

LaTeX Lean

MainProofs.bohman_limit_cycles

Theorem 208

LaTeX Lean

MainProofs.bohman_limit_fraction_graphs

Theorem 206

LaTeX Lean

MainProofs.bohman_limit_fractionGraph_two

Theorem 207

LaTeX Lean

MainProofs.construction_addSubgroupCapacity_bound

Theorem 204

LaTeX Lean

MainProofs.construction_gives_shannon_bound

Theorem 201

LaTeX Lean

MainProofs.construction_lower_bound

Theorem 200

LaTeX Lean

MainProofs.Delta

Definition 202

LaTeX Lean

MainProofs.delta_bound

Theorem 203

LaTeX Lean

MainProofs.denom_pos_rat

Theorem 193

LaTeX Lean

MainProofs.det_B_eq_p_int

Theorem 199

LaTeX Lean

MainProofs.matrixA_entries_integral

Theorem 191

LaTeX Lean

MainProofs.matrixB_entries_integral

Theorem 192

LaTeX Lean

MainProofs.minDist_A_ge_q_int

Theorem 198

LaTeX Lean

MainProofs.p_is_pos_nat

Theorem 195

LaTeX Lean

MainProofs.q_is_pos_nat

Theorem 196

LaTeX Lean

MainProofs.subgroup_capacity_limit

Theorem 205

LaTeX Lean

MAlpha.det_xRα_add_yI

Theorem 120

LaTeX Lean

MAlpha.Dα

Definition 115

LaTeX Lean

MAlpha.Dα_inv

Theorem 132

LaTeX Lean

MAlpha.Dα_Mα_conjugation

Theorem 134

LaTeX Lean

MAlpha.Dα_Rα_conjugation

Theorem 133

LaTeX Lean

MAlpha.minor00_diag

Theorem 117

LaTeX Lean

MAlpha.minor00_lowerTriangular

Theorem 116

LaTeX Lean

MAlpha.minor0n_diag

Theorem 119

LaTeX Lean

MAlpha.minor0n_upperTriangular

Theorem 118

LaTeX Lean

MAlpha.Mα

Definition 113

LaTeX Lean

MAlpha.Mα_det

Theorem 128

LaTeX Lean

MAlpha.Mα_det_nonneg

Theorem 129

LaTeX Lean

MAlpha.Mα_factorization

Theorem 127

LaTeX Lean

MAlpha.Mα_isP0

Theorem 131

LaTeX Lean

MAlpha.Mα_mul_Rα_sub_one

Theorem 126

LaTeX Lean

MAlpha.Mα_mul_Rα_sub_one_corner

Theorem 124

LaTeX Lean

MAlpha.Mα_mul_Rα_sub_one_diag

Theorem 122

LaTeX Lean

MAlpha.Mα_mul_Rα_sub_one_other

Theorem 125

LaTeX Lean

MAlpha.Mα_mul_Rα_sub_one_subdiag

Theorem 123

LaTeX Lean

MAlpha.Mα_principalSubmatrix

Theorem 130

LaTeX Lean

MAlpha.Rα

Definition 114

LaTeX Lean

MAlpha.Rα_sub_one_isUnit

Theorem 121

LaTeX Lean

P0Matrix.continuous_principalSubmatrix

Theorem 109

LaTeX Lean

P0Matrix.continuous_principalSubmatrix_det

Theorem 110

LaTeX Lean

P0Matrix.det_add_diagonal

Theorem 95

LaTeX Lean

P0Matrix.fixingPermEquiv

Definition 90

LaTeX Lean

P0Matrix.isClosed_principalMinor_nonneg

Theorem 111

LaTeX Lean

P0Matrix.isP0_closed

Theorem 112

LaTeX Lean

P0Matrix.isP0_diagonal_left

Theorem 107

LaTeX Lean

P0Matrix.isP0_diagonal_right

Theorem 108

LaTeX Lean

P0Matrix.isP0_principalSubmatrix

Theorem 97

LaTeX Lean

P0Matrix.isP0_smul_pos

Theorem 104

LaTeX Lean

P0Matrix.IsP0Matrix

Definition 86

LaTeX Lean

P0Matrix.orderEmbEquiv

Definition 89

LaTeX Lean

P0Matrix.orderEmbOfFin_fixingPermEquiv

Theorem 92

LaTeX Lean

P0Matrix.p0_add_pos_diagonal_det_pos

Theorem 99

LaTeX Lean

P0Matrix.p0_add_scalar_invertible

Theorem 101

LaTeX Lean

P0Matrix.p0_min_distance_bound

Theorem 102

LaTeX Lean

P0Matrix.p0_sign_property

Theorem 100

LaTeX Lean

P0Matrix.perm_mem_of_fixing

Theorem 88

LaTeX Lean

P0Matrix.principalSubmatrix

Definition 85

LaTeX Lean

P0Matrix.principalSubmatrix_diagonal_mul

Theorem 105

LaTeX Lean

P0Matrix.principalSubmatrix_empty_det

Theorem 96

LaTeX Lean

P0Matrix.principalSubmatrix_mul_diagonal

Theorem 106

LaTeX Lean

P0Matrix.principalSubmatrix_mulVec

Theorem 98

LaTeX Lean

P0Matrix.principalSubmatrix_smul

Theorem 103

LaTeX Lean

P0Matrix.prod_ite_sigma_eq

Theorem 87

LaTeX Lean

P0Matrix.prod_of_fixing

Theorem 93

LaTeX Lean

P0Matrix.sign_of_fixing

Theorem 91

LaTeX Lean

P0Matrix.sum_fixing_eq_det

Theorem 94

LaTeX Lean

shannonCapacity

Definition 12

LaTeX Lean

shannonCapacity_bddAbove

Theorem 19

LaTeX Lean

shannonCapacity_fractionGraph_eq_of_eq

Theorem 49

LaTeX Lean

shannonCapacity_fractionGraph_le

Theorem 47

LaTeX Lean

shannonCapacity_fractionGraph_mono

Theorem 48

LaTeX Lean

shannonCapacity_ge_root

Theorem 20

LaTeX Lean

shannonCapacity_iso

Theorem 13

LaTeX Lean

shannonCapacity_le_of_cohomomorphism

Theorem 28

LaTeX Lean

strongPower

Definition 1

LaTeX Lean

strongPower_cohomomorphism_of_cohomomorphism

Theorem 27

LaTeX Lean

strongPower_isClique_piFinset

Theorem 11

LaTeX Lean

strongPower_iso

Definition 10

LaTeX Lean

sub_mul_div_le

Theorem 31

LaTeX Lean

subgroupIndependenceNumber

Definition 14

LaTeX Lean

subgroupShannonCapacity

Definition 15

LaTeX Lean

zmod_sub_eq_one_of_fin_sub_eq_one

Theorem 40

LaTeX Lean