Int

📁 Source: Mathlib/LinearAlgebra/FreeModule/Int.lean

Statistics

Metric	Count
Definitions	0
Theorems addSubgroup_index_ne_zero_iff, subgroup_index_ne_zero_iff, submodule_toAddSubgroup_index_ne_zero_iff, toAddSubgroup_index_eq_ite, toAddSubgroup_index_eq_pow_mul_prod, toAddSubgroup_index_ne_zero_iff	6
Total	6

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addSubgroup_index_ne_zero_iff 📖	mathematical	—	AddEquiv AddSubgroup Pi.addGroup instAddGroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.add Pi.instAdd	—	RingHomInvPair.ids submodule_toAddSubgroup_index_ne_zero_iff
subgroup_index_ne_zero_iff 📖	mathematical	—	MulEquiv Subgroup Pi.group Multiplicative Multiplicative.group instAddGroup SetLike.instMembership Subgroup.instSetLike Subgroup.mul Pi.instMul Multiplicative.mul	—	MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass Subgroup.comap_equiv_eq_map_symm Subgroup.index_comap_of_surjective MulEquiv.surjective Subgroup.index_toAddSubgroup addSubgroup_index_ne_zero_iff
submodule_toAddSubgroup_index_ne_zero_iff 📖	mathematical	—	LinearEquiv instSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Submodule Pi.addCommMonoid instAddCommMonoid AddCommGroup.toIntModule Pi.addCommGroup instAddCommGroup SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.addCommGroup instRing	—	RingHomInvPair.ids instIsDomain EuclideanDomain.to_principal_ideal_domain Module.Basis.SmithNormalForm.toAddSubgroup_index_ne_zero_iff card_eq_of_linearEquiv invariantBasisNumber_of_nontrivial_of_commRing instNontrivial RingHomCompTriple.ids Finite.of_fintype Fintype.card_fin

Module.Basis.SmithNormalForm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toAddSubgroup_index_eq_ite 📖	mathematical	—	AddSubgroup.index AddCommGroup.toAddGroup Submodule.toAddSubgroup CommRing.toRing Fintype.card Finset.prod Nat.instCommMonoid Finset.univ Fin.fintype Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring Ideal.span Set Set.instSingletonSet a	—	toAddSubgroup_index_eq_pow_mul_prod Nat.card_eq_zero_of_infinite tsub_self Nat.instCanonicallyOrderedAdd Nat.instOrderedSub pow_zero one_mul Ne.lt_of_le Fintype.card_fin Fintype.card_le_of_embedding MulZeroClass.zero_mul
toAddSubgroup_index_eq_pow_mul_prod 📖	mathematical	—	AddSubgroup.index AddCommGroup.toAddGroup Submodule.toAddSubgroup CommRing.toRing Monoid.toNatPow Nat.instMonoid Nat.card Fintype.card Finset.prod Nat.instCommMonoid Finset.univ Fin.fintype Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring Ideal.span Set Set.instSingletonSet a	—	RingHomSurjective.ids RingHomInvPair.ids Finite.of_fintype RingHomSurjective.invPair LinearEquiv.submoduleMap_apply map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Module.Basis.repr_self Finsupp.single_eq_pi_single Pi.single_apply mul_ite mul_one MulZeroClass.mul_zero SemilinearEquivClass.toAddEquivClass AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass AddEquiv.surjective AddSubgroup.comap_equiv_eq_map_symm LinearEquiv.coe_toAddEquiv_symm AddEquiv.symm_symm Submodule.map_toAddSubgroup AddSubgroup.index_comap_of_surjective AddSubgroup.ext Module.Basis.mem_submodule_iff' Finset.sum_congr Finset.sum_apply Finset.sum_eq_single Function.Embedding.injective instIsEmptyFalse dvd_mul_left Finset.sum_const_zero dvd_refl Function.instEmbeddingLikeEmbedding Classical.choose_eq smul_ite smul_zero mul_comm zero_dvd_iff Ideal.span_zero AddSubgroup.index_pi Finset.prod_congr AddSubgroup.index_bot Finset.prod_dite Finset.prod_const Finset.card_attach Finset.compl_filter Fintype.card_fin Finset.univ_filter_exists Finset.card_image_of_injective Finset.card_compl Finset.attach_eq_univ Finset.ext Finset.prod_map
toAddSubgroup_index_ne_zero_iff 📖	mathematical	—	Fintype.card	—	toAddSubgroup_index_eq_ite Int.infinite Finset.prod_congr Module.Basis.ne_zero Int.instNontrivial AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass zero_smul Ideal.span_singleton_toAddSubgroup_eq_zmultiples Int.index_zmultiples Nat.instNontrivial IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd

---

← Back to Index