Documentation Verification Report

GaussEisensteinLemmas

📁 Source: Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean

Statistics

Metric	Count
Definitions	0
Theorems `Ico_map_valMinAbs_natAbs_eq_Ico_map_id`, `div_eq_filter_card`, `eisenstein_lemma`, `eisenstein_lemma_aux`, `gauss_lemma`, `gauss_lemma_aux`, `sum_mul_div_add_sum_mul_div_eq_mul`	7
Total	7

ZMod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Ico_map_valMinAbs_natAbs_eq_Ico_map_id` 📖	mathematical	—	`Multiset.map` `valMinAbs` `ZMod` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `Finset.val` `Finset.Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder`	—	`lt_of_le_of_lt` `Nat.Prime.pos` `Fact.out` `not_lt_of_ge` `IsDomain.to_noZeroDivisors` `instIsDomain` `CharP.cast_eq_zero_iff` `charP` `Nat.instNoMaxOrder` `natAbs_valMinAbs_le` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `Finset.mem_Ico` `div_eq_mul_inv` `natCast_natAbs_valMinAbs` `mul_div_cancel₀` `valMinAbs_def_pos` `val_cast_of_lt` `mul_neg` `natAbs_valMinAbs_neg` `Multiset.map_eq_map_of_bij_of_nodup` `Finset.nodup` `Finset.inj_on_of_surj_on_of_card_le` `le_rfl`
`div_eq_filter_card` 📖	mathematical	—	`Finset.card` `Finset.filter` `Finset.Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder`	—	`Nat.card_Ico` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Finset.ext` `le_trans` `Nat.instNoMaxOrder`
`eisenstein_lemma` 📖	mathematical	—	`legendreSym` `Monoid.toNatPow` `Int.instMonoid` `Finset.sum` `Nat.instAddCommMonoid` `Finset.Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder`	—	`Nat.cast_zero` `Int.cast_zero` `Int.cast_natCast` `neg_one_pow_eq_pow_mod_two` `gauss_lemma` `eisenstein_lemma_aux` `Nat.Prime.mod_two_eq_one_iff_ne_two` `Fact.out`
`eisenstein_lemma_aux` 📖	mathematical	—	`Nat.ModEq` `Finset.card` `Finset.filter` `val` `ZMod` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `Finset.Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `Finset.sum` `Nat.instAddCommMonoid`	—	`Nat.fact_prime_two` `natCast_eq_natCast_iff` `sub_eq_zero` `Finset.sum_congr` `mul_comm` `Nat.cast_sum` `sub_eq_add_neg` `neg_eq_self_mod_two` `add_assoc` `add_left_comm` `Nat.cast_mul` `Nat.cast_one` `mul_one` `AddLeftCancelSemigroup.toIsLeftCancelAdd`
`gauss_lemma` 📖	mathematical	—	`legendreSym` `Monoid.toNatPow` `Int.instMonoid` `Finset.card` `Finset.filter` `val` `ZMod` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Finset.Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder`	—	`Nat.Prime.odd_of_ne_two` `Fact.out` `legendreSym.eq_pow` `gauss_lemma_aux` `legendreSym.eq_one_or_neg_one` `neg_one_pow_eq_or` `Int.cast_one` `Int.cast_neg` `ne_neg_self` `one_ne_zero` `NeZero.one` `nontrivial` `Nat.Prime.one_lt'`
`gauss_lemma_aux` 📖	mathematical	—	`ZMod` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Int.instMonoid` `Finset.card` `Finset.filter` `val` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Finset.Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder`	—	`mul_left_inj'` `IsCancelMulZero.toIsRightCancelMulZero` `IsDomain.toIsCancelMulZero` `instIsDomain` `CharP.cast_eq_zero_iff` `charP` `Nat.Prime.dvd_factorial` `Fact.out` `not_le` `Nat.Prime.pos` `Int.cast_pow` `Int.cast_neg` `Int.cast_one` `Finset.filter.congr_simp`
`sum_mul_div_add_sum_mul_div_eq_mul` 📖	mathematical	—	`Finset.sum` `Nat.instAddCommMonoid` `Finset.Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder`	—	`Finset.card_equiv` `Finset.disjoint_filter` `lt_of_le_of_lt` `Nat.Prime.pos` `Fact.out` `Nat.cast_mul` `CharP.cast_eq_zero` `charP` `MulZeroClass.mul_zero` `IsDomain.to_noZeroDivisors` `instIsDomain` `le_antisymm` `val_zero` `val_cast_of_lt` `Nat.instCanonicallyOrderedAdd` `Finset.ext` `le_total` `Finset.card_union_of_disjoint` `Finset.card_product` `Nat.card_Ico` `tsub_zero` `Nat.instOrderedSub`

---

← Back to Index