Documentation Verification Report

Finite

📁 Source: Mathlib/NumberTheory/ClassNumber/Finite.lean

Statistics

Metric	Count
Definitions `cardM`, `distinctElems`, `finsetApprox`, `fintypeOfAdmissibleOfAlgebraic`, `fintypeOfAdmissibleOfFinite`, `mkMMem`, `normBound`	7
Theorems `exists_mem_finsetApprox`, `exists_mem_finset_approx'`, `exists_min`, `exists_mk0_eq_mk0`, `zero_notMem`, `mem_finsetApprox`, `mkMMem_surjective`, `ne_bot_of_prod_finsetApprox_mem`, `normBound_pos`, `norm_le`, `norm_lt`, `prod_finsetApprox_ne_zero`	12
Total	19

ClassGroup

Definitions

Name	Category	Theorems
`cardM` 📖	CompOp	1 math math: `mem_finsetApprox`
`distinctElems` 📖	CompOp	1 math math: `mem_finsetApprox`
`finsetApprox` 📖	CompOp	6 math math: `mkMMem_surjective`, `exists_mk0_eq_mk0`, `finsetApprox.zero_notMem`, `mem_finsetApprox`, `exists_mem_finset_approx'`, `exists_mem_finsetApprox`
`fintypeOfAdmissibleOfAlgebraic` 📖	CompOp	—
`fintypeOfAdmissibleOfFinite` 📖	CompOp	—
`mkMMem` 📖	CompOp	1 math math: `mkMMem_surjective`
`normBound` 📖	CompOp	3 math math: `normBound_pos`, `norm_lt`, `norm_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_mem_finsetApprox` 📖	mathematical	—	`Finset` `Finset.instMembership` `finsetApprox` `DFunLike.coe` `AbsoluteValue` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Int.instSemiring` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `AbsoluteValue.funLike` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommRing.toRing` `MonoidHom.instFunLike` `Algebra.norm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Algebra.toSMul` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`Fintype.card_pos_iff` `Module.Basis.index_nonempty` `IsDomain.toNontrivial` `Real.rpow_pos_of_pos` `Int.cast_pos` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `normBound_pos` `AbsoluteValue.nonneg` `Algebra.smul_def` `eq_intCast` `RingHom.instRingHomClass` `Real.mul_rpow` `Int.cast_nonneg` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Nat.cast_one` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Linarith.add_neg` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.without_one_mul` `CancelDenoms.sub_subst` `Real.rpow_mul` `Int.cast_zero` `div_mul_cancel₀` `Real.rpow_neg_one` `mul_left_comm` `mul_inv_cancel₀` `mul_one` `Real.rpow_natCast` `le_refl` `RingHomInvPair.ids` `EuclideanDomain.div_add_mod` `Module.Basis.sum_repr` `Finset.smul_sum` `Finset.sum_congr` `SemigroupAction.mul_smul` `add_smul` `AbsoluteValue.IsAdmissible.exists_approx` `mem_finsetApprox` `sub_smul` `smul_sub` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Algebra.norm_algebraMap_of_basis` `AbsoluteValue.map_pow` `Int.instIsDomain` `EuclideanDomain.toNontrivial` `Int.cast_lt` `LT.lt.trans_le` `norm_lt` `lt_of_le_of_lt` `le_of_eq` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `map_sub` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `Finset.sum_apply'` `Finset.sum_sub_distrib` `Module.Basis.repr_self_apply` `mul_boole` `Finset.sum_ite_eq'`
`exists_mem_finset_approx'` 📖	mathematical	—	`Finset` `Finset.instMembership` `finsetApprox` `DFunLike.coe` `AbsoluteValue` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Int.instSemiring` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `AbsoluteValue.funLike` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommRing.toRing` `MonoidHom.instFunLike` `Algebra.norm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Algebra.toSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Algebra.IsAlgebraic.exists_smul_eq_mul` `IsDomain.to_noZeroDivisors` `exists_mem_finsetApprox` `lt_of_mul_lt_mul_left` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Int.instIsStrictOrderedRing` `lt_of_le_of_lt` `le_of_eq` `AbsoluteValue.map_mul` `map_mul` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `Algebra.smul_def` `smul_sub` `sub_mul` `SMulCommClass.smul_comm` `smulCommClass_self` `mul_comm` `Algebra.smul_mul_assoc` `mul_lt_mul` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `IsStrictOrderedRing.toMulPosStrictMono` `le_rfl` `AbsoluteValue.pos` `Algebra.norm_ne_zero_iff_of_basis` `Finite.of_fintype` `EuclideanDomain.instIsDomain` `AbsoluteValue.nonneg`
`exists_min` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Submonoid.instSetLike` `nonZeroDivisors` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Int.exists_least_of_bdd` `AbsoluteValue.nonneg` `Submodule.ne_bot_iff` `nonZeroDivisors.coe_ne_zero` `Ideal.instNontrivial` `IsDomain.toNontrivial` `Mathlib.Tactic.Contrapose.contrapose₁`
`exists_mk0_eq_mk0` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors` `ClassGroup` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instCommGroupClassGroup` `MonoidHom.instFunLike` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom` `EuclideanDomain.toCommRing` `RingHom.instFunLike` `algebraMap` `Finset.prod` `CommRing.toCommMonoid` `finsetApprox`	—	`prod_finsetApprox_ne_zero` `exists_min` `IsScalarTower.right` `Ideal.dvd_iff_le` `IsScalarTower.left` `Ideal.mul_le` `Ideal.mem_span_singleton` `exists_mem_finset_approx'` `dvd_of_mul_left_dvd` `sub_eq_zero` `Ideal.sub_mem` `Ideal.mul_mem_left` `Algebra.smul_def` `mul_dvd_mul_right` `dvd_trans` `map_dvd` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `Multiset.dvd_prod` `Multiset.mem_map` `mem_nonZeroDivisors_iff_ne_zero` `Ideal.instNoZeroDivisors` `IsDomain.to_noZeroDivisors` `Ideal.instNontrivial` `IsDomain.toNontrivial` `Ideal.span_singleton_eq_bot` `Ideal.mul_bot` `Ideal.zero_eq_bot` `SetLike.mem_coe` `Set.singleton_subset_iff` `Ideal.span_le` `mul_dvd_mul_iff_left` `IsCancelMulZero.toIsLeftCancelMulZero` `Ideal.isCancelMulZero` `mul_comm` `Ideal.mul_mono` `le_rfl`
`mem_finsetApprox` 📖	mathematical	—	`Finset` `Finset.instMembership` `finsetApprox` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `EuclideanDomain.toCommRing` `DFunLike.coe` `Function.Embedding` `cardM` `Function.instFunLikeEmbedding` `distinctElems`	—	`sub_self` `sub_eq_zero` `Function.Embedding.injective` `Finset.mem_univ`
`mkMMem_surjective` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `DFunLike.coe` `RingHom` `EuclideanDomain.toCommRing` `RingHom.instFunLike` `algebraMap` `Finset.prod` `CommRing.toCommMonoid` `finsetApprox` `ClassGroup` `mkMMem`	—	`exists_mk0_eq_mk0`
`ne_bot_of_prod_finsetApprox_mem` 📖	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `DFunLike.coe` `RingHom` `EuclideanDomain.toCommRing` `RingHom.instFunLike` `algebraMap` `Finset.prod` `CommRing.toCommMonoid` `finsetApprox`	—	—	`Submodule.ne_bot_iff` `prod_finsetApprox_ne_zero`
`normBound_pos` 📖	mathematical	—	`normBound`	—	`Module.Basis.index_nonempty` `IsDomain.toNontrivial` `Module.Basis.ne_zero` `EuclideanDomain.toNontrivial` `injective_iff_map_eq_zero` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Algebra.leftMulMatrix_injective` `Matrix.ext` `Algebra.smul_def` `eq_natCast` `RingHom.instRingHomClass` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Int.instIsStrictOrderedRing` `Nat.factorial_pos` `pow_pos` `Int.instZeroLEOneClass` `Fintype.card_pos_iff` `lt_of_lt_of_le` `AbsoluteValue.pos` `Finset.le_max'` `Finset.mem_image` `Finset.mem_univ`
`norm_le` 📖	mathematical	`DFunLike.coe` `AbsoluteValue` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Int.instSemiring` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `AbsoluteValue.funLike` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finsupp.instAddCommMonoid` `Algebra.toModule` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr`	`MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Ring.toSemiring` `CommRing.toRing` `MonoidHom.instFunLike` `Algebra.norm` `normBound` `Monoid.toNatPow` `Int.instMonoid` `Fintype.card`	—	`RingHomInvPair.ids` `Module.Basis.sum_repr` `smulCommClass_self` `IsScalarTower.left` `Algebra.norm_apply` `Finite.of_fintype` `LinearMap.det_toMatrix` `Matrix.det.congr_simp` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Finset.sum_congr` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `smul_mul_assoc` `IsScalarTower.right` `Finset.card_univ` `mul_comm` `Matrix.det_sum_smul_le` `EuclideanDomain.toNontrivial` `Int.instIsStrictOrderedRing` `Finset.le_max'` `Finset.mem_image` `Finset.mem_univ`
`norm_lt` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `DFunLike.coe` `AbsoluteValue` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Int.instSemiring` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `instConditionallyCompleteLinearOrder` `AbsoluteValue.funLike` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finsupp.instAddCommMonoid` `Algebra.toModule` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr`	`MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Ring.toSemiring` `CommRing.toRing` `MonoidHom.instFunLike` `Algebra.norm` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `normBound` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Fintype.card`	—	`RingHomInvPair.ids` `Module.Basis.index_nonempty` `IsDomain.toNontrivial` `Finset.mem_image` `Finset.mem_univ` `Finset.le_max'` `Finset.Nonempty.image` `Finset.Nonempty.of_image` `Finset.max'_image` `Int.cast_le` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Finset.max'_lt_iff` `le_trans` `AbsoluteValue.nonneg` `LE.le.trans_lt` `norm_le` `Int.cast_mul` `Int.cast_pow` `mul_lt_mul'` `IsStrictOrderedRing.toPosMulStrictMono` `IsOrderedRing.toMulPosMono` `le_rfl` `pow_lt_pow_left₀` `Int.cast_nonneg` `Fintype.card_ne_zero` `pow_nonneg` `IsOrderedRing.toPosMulMono` `Int.cast_pos` `normBound_pos`
`prod_finsetApprox_ne_zero` 📖	—	—	—	—	`injective_iff_map_eq_zero` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Module.Basis.algebraMap_injective` `EuclideanDomain.instIsDomain` `IsDomain.toNontrivial` `EuclideanDomain.toNontrivial` `IsDomain.to_noZeroDivisors` `finsetApprox.zero_notMem`

ClassGroup.finsetApprox

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`zero_notMem` 📖	mathematical	—	`Finset` `Finset.instMembership` `ClassGroup.finsetApprox` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing`	—	`Finset.notMem_erase`

---

← Back to Index