CardQuotient

📁 Source: Mathlib/LinearAlgebra/FreeModule/Finite/CardQuotient.lean

Statistics

Metric	Count
Definitions	0
Theorems index_eq_natAbs_det, relIndex_eq_abs_det, relIndex_eq_natAbs_det, natAbs_det_basis_change, natAbs_det_equiv	5
Total	5

AddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
index_eq_natAbs_det 📖	mathematical	—	index AddCommGroup.toAddGroup DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommRing AddCommGroup.toAddCommMonoid AddCommGroup.toIntModule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instFunLike Module.Basis.det AddSubgroup SetLike.instMembership instSetLike Module.Basis Int.instSemiring toAddCommGroup Module.Basis.instFunLike	—	Module.Free.of_basis Module.Finite.of_basis Finite.of_fintype Submodule.natAbs_det_basis_change
relIndex_eq_abs_det 📖	mathematical	AddSubgroup AddCommGroup.toAddGroup Preorder.toLE PartialOrder.toPreorder instPartialOrder closure Set.range DFunLike.coe Module.Basis Rat.semiring AddCommGroup.toAddCommMonoid Module.Basis.instFunLike	relIndex abs Rat.instLattice Rat.addGroup AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring Rat.commRing NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instFunLike Module.Basis.det	—	Rat.nontrivial instIsAddTorsionFreeOfAddLeftStrictMonoOfAddRightStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Rat.instAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add SetLike.coe_mem relIndex_eq_natAbs_det Nat.cast_natAbs Int.cast_abs Rat.instIsStrictOrderedRing Module.Basis.det_apply RingHom.map_det Matrix.ext RingHomInvPair.ids Module.Basis.addSubgroupOfClosure_apply Module.Basis.addSubgroupOfClosure_repr_apply
relIndex_eq_natAbs_det 📖	mathematical	AddSubgroup AddCommGroup.toAddGroup Preorder.toLE PartialOrder.toPreorder instPartialOrder	relIndex DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommRing Submodule Int.instSemiring AddCommGroup.toAddCommMonoid AddCommGroup.toIntModule SetLike.instMembership Submodule.setLike OrderIso Submodule.instPartialOrder instFunLikeOrderIso toIntSubmodule Submodule.addCommGroup Int.instRing NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instFunLike Module.Basis.det Module.Basis Submodule.addCommMonoid Module.Basis.instFunLike SetLike.coe_mem instSetLike	—	SetLike.coe_mem relIndex.eq_1 RingHomInvPair.ids index_eq_natAbs_det

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
natAbs_det_basis_change 📖	mathematical	—	DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommRing AddCommGroup.toAddCommMonoid AddCommGroup.toIntModule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instFunLike Module.Basis.det Submodule Int.instSemiring SetLike.instMembership setLike Module.Basis addCommMonoid addCommGroup Int.instRing Module.Basis.instFunLike Nat.card HasQuotient.Quotient hasQuotient	—	RingHomInvPair.ids RingHomCompTriple.ids Module.Basis.det_comp_basis natAbs_det_equiv SemilinearEquivClass.toAddEquivClass LinearEquiv.instSemilinearEquivClass
natAbs_det_equiv 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddCommGroup.toIntModule MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det LinearMap.comp Submodule Int.instSemiring SetLike.instMembership setLike addCommMonoid module RingHomCompTriple.ids subtype AddMonoidHom.toIntLinearMap addCommGroup Int.instRing AddMonoidHomClass.toAddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup EquivLike.toFunLike AddEquivClass.instAddMonoidHomClass Nat.card HasQuotient.Quotient hasQuotient	—	LinearEquiv.finrank_eq RingHomInvPair.ids Int.instIsDomain EuclideanDomain.to_principal_ideal_domain Finite.of_fintype smithNormalFormBotBasis_def RingHomCompTriple.ids Module.Basis.equiv_apply Equiv.refl_apply smulCommClass_self LinearMap.det_toMatrix Matrix.ext LinearMap.toMatrix_apply map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Module.Basis.repr_self Finsupp.smul_single smul_eq_mul mul_one Matrix.diagonal_apply_eq Finsupp.single_eq_same Matrix.diagonal_apply_ne Finsupp.single_eq_of_ne Matrix.det_diagonal map_prod MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass Nat.card_congr Nat.card_pi Finset.prod_congr Nat.card_zmod Int.natAbs_eq_iff_associated LinearMap.associated_det_comp_equiv

---

← Back to Index