Documentation Verification Report

ADEInequality

📁 Source: Mathlib/NumberTheory/ADEInequality.lean

Statistics

Metric	Count
Definitions `A`, `A'`, `Admissible`, `D'`, `E'`, `E6`, `E7`, `E8`, `sumInv`	9
Theorems `one_lt_sumInv`, `admissible_A'`, `admissible_D'`, `admissible_E'3`, `admissible_E'4`, `admissible_E'5`, `admissible_E6`, `admissible_E7`, `admissible_E8`, `admissible_of_one_lt_sumInv`, `admissible_of_one_lt_sumInv_aux`, `admissible_of_one_lt_sumInv_aux'`, `classification`, `lt_four`, `lt_six`, `lt_three`, `sumInv_pqr`	17
Total	26

ADEInequality

Definitions

Name	Category	Theorems
`A` 📖	CompOp	—
`A'` 📖	CompOp	1 math math: `admissible_A'`
`Admissible` 📖	MathDef	12 math math: `admissible_E7`, `admissible_of_one_lt_sumInv`, `admissible_of_one_lt_sumInv_aux`, `admissible_E6`, `admissible_of_one_lt_sumInv_aux'`, `admissible_E'4`, `admissible_A'`, `admissible_E'5`, `admissible_E8`, `classification`, `admissible_E'3`, `admissible_D'`
`D'` 📖	CompOp	1 math math: `admissible_D'`
`E'` 📖	CompOp	3 math math: `admissible_E'4`, `admissible_E'5`, `admissible_E'3`
`E6` 📖	CompOp	1 math math: `admissible_E6`
`E7` 📖	CompOp	1 math math: `admissible_E7`
`E8` 📖	CompOp	1 math math: `admissible_E8`
`sumInv` 📖	CompOp	3 math math: `sumInv_pqr`, `Admissible.one_lt_sumInv`, `classification`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`admissible_A'` 📖	mathematical	—	`Admissible` `A'`	—	—
`admissible_D'` 📖	mathematical	—	`Admissible` `D'`	—	—
`admissible_E'3` 📖	mathematical	—	`Admissible` `E'` `PNat` `instOfNatPNatOfNeZeroNat`	—	—
`admissible_E'4` 📖	mathematical	—	`Admissible` `E'` `PNat` `instOfNatPNatOfNeZeroNat`	—	—
`admissible_E'5` 📖	mathematical	—	`Admissible` `E'` `PNat` `instOfNatPNatOfNeZeroNat`	—	—
`admissible_E6` 📖	mathematical	—	`Admissible` `E6`	—	`admissible_E'3`
`admissible_E7` 📖	mathematical	—	`Admissible` `E7`	—	`admissible_E'4`
`admissible_E8` 📖	mathematical	—	`Admissible` `E8`	—	`admissible_E'5`
`admissible_of_one_lt_sumInv` 📖	mathematical	`sumInv` `PNat` `Multiset` `Multiset.instInsert` `Multiset.instSingleton`	`Admissible`	—	`instIsTransLe` `instAntisymmLe` `LE.total` `List.Pairwise.sortedLE` `Multiset.pairwise_sort` `Multiset.sort_eq` `admissible_of_one_lt_sumInv_aux` `Multiset.length_sort` `Multiset.card_cons` `Multiset.card_singleton`
`admissible_of_one_lt_sumInv_aux` 📖	mathematical	`List.SortedLE` `PNat` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `sumInv` `Multiset.ofList`	`Admissible`	—	`instIsEmptyFalse` `List.SortedLE.pairwise` `admissible_of_one_lt_sumInv_aux'`
`admissible_of_one_lt_sumInv_aux'` 📖	mathematical	`PNat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `sumInv` `Multiset` `Multiset.instInsert` `Multiset.instSingleton`	`Admissible`	—	`lt_three` `Finset.mem_Iio` `admissible_A'` `lt_four` `Finset.mem_Ico` `admissible_D'` `lt_six` `admissible_E6` `admissible_E7` `admissible_E8`
`classification` 📖	mathematical	—	`sumInv` `PNat` `Multiset` `Multiset.instInsert` `Multiset.instSingleton` `Admissible`	—	`admissible_of_one_lt_sumInv` `Admissible.one_lt_sumInv`
`lt_four` 📖	mathematical	`PNat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `sumInv` `Multiset` `Multiset.instInsert` `instOfNatPNatOfNeZeroNat` `Multiset.instSingleton`	`Preorder.toLT`	—	`Nat.instAtLeastTwoHAddOfNat` `IsStrictOrderedRing.toIsOrderedRing` `Rat.instIsStrictOrderedRing` `Rat.nontrivial` `Mathlib.Tactic.Contrapose.contrapose₁` `sumInv_pqr` `LE.le.trans` `inv_le_inv₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Rat.instAddLeftMono` `Rat.instZeroLEOneClass` `Rat.instCharZero` `add_le_add` `covariant_swap_add_of_covariant_add` `le_rfl` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_add` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat`
`lt_six` 📖	mathematical	`sumInv` `PNat` `Multiset` `Multiset.instInsert` `instOfNatPNatOfNeZeroNat` `Multiset.instSingleton`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat`	—	`Nat.instAtLeastTwoHAddOfNat` `IsStrictOrderedRing.toIsOrderedRing` `Rat.instIsStrictOrderedRing` `Rat.nontrivial` `Mathlib.Tactic.Contrapose.contrapose₁` `sumInv_pqr` `inv_le_inv₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Rat.instAddLeftMono` `Rat.instZeroLEOneClass` `Rat.instCharZero` `add_le_add` `covariant_swap_add_of_covariant_add` `le_rfl` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_add` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat`
`lt_three` 📖	mathematical	`PNat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `sumInv` `Multiset` `Multiset.instInsert` `Multiset.instSingleton`	`Preorder.toLT` `instOfNatPNatOfNeZeroNat`	—	`Nat.instAtLeastTwoHAddOfNat` `IsStrictOrderedRing.toIsOrderedRing` `Rat.instIsStrictOrderedRing` `Rat.nontrivial` `Mathlib.Tactic.Contrapose.contrapose₁` `sumInv_pqr` `LE.le.trans` `inv_le_inv₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Rat.instAddLeftMono` `Rat.instZeroLEOneClass` `Rat.instCharZero` `add_le_add` `covariant_swap_add_of_covariant_add` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_add` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat`
`sumInv_pqr` 📖	mathematical	—	`sumInv` `PNat` `Multiset` `Multiset.instInsert` `Multiset.instSingleton` `PNat.val`	—	`Multiset.map_cons` `Multiset.sum_cons` `Multiset.sum_singleton` `add_assoc`

ADEInequality.Admissible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`one_lt_sumInv` 📖	mathematical	`ADEInequality.Admissible`	`ADEInequality.sumInv`	—	`eq_1` `ADEInequality.A'.eq_1` `ADEInequality.sumInv_pqr` `add_assoc` `Nat.cast_one` `inv_one` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Rat.instAddLeftMono` `contravariant_lt_of_covariant_le` `add_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Rat.instIsStrictOrderedRing` `IsStrictOrderedRing.toIsOrderedRing` `Rat.nontrivial` `ADEInequality.D'.eq_1` `Mathlib.Meta.NormNum.IsNNRat.to_eq` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Rat.instCharZero` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `add_halves` `ZeroLEOneClass.neZero.two` `Rat.instZeroLEOneClass` `NeZero.charZero_one` `ADEInequality.E'.eq_1` `Mathlib.Meta.NormNum.isNNRat_add` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNNRat_lt_true` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero`

---

← Back to Index