Commensurable

📁 Source: Mathlib/GroupTheory/Commensurable.lean

Statistics

Metric	Count
Definitions Commensurable, Commensurable, quotConjEquiv, Commensurable, commensurator, commensurator', quotConjEquiv	7
Theorems comm, equivalence, refl, trans, comm, commensurable_conj, commensurable_inv, commensurator'_mem_iff, commensurator_mem_iff, conj, eq, equivalence, refl, trans	14
Total	21

AddSubgroup

Definitions

Name	Category	Theorems
Commensurable 📖	MathDef	4 math math: Subgroup.commensurable_strictPeriods_periods, Commensurable.comm, Commensurable.refl, Commensurable.equivalence

AddSubgroup.Commensurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comm 📖	mathematical	—	AddSubgroup.Commensurable	—	—
equivalence 📖	mathematical	—	AddSubgroup AddSubgroup.Commensurable	—	refl symm trans
refl 📖	mathematical	—	AddSubgroup.Commensurable	—	AddSubgroup.relIndex_self one_ne_zero
trans 📖	—	AddSubgroup.Commensurable	—	—	AddSubgroup.relIndex_ne_zero_trans

Commensurable

Definitions

Name	Category	Theorems
quotConjEquiv 📖	CompOp	—

Subgroup

Definitions

Name	Category	Theorems
Commensurable 📖	MathDef	9 math math: Commensurable.comm, IsArithmetic.is_commensurable, Commensurable.commensurable_conj, commensurable_adjoinNegOne_self, Commensurable.commensurator_mem_iff, Commensurable.commensurable_inv, Commensurable.commensurator'_mem_iff, Commensurable.refl, Commensurable.equivalence
quotConjEquiv 📖	CompOp	—

Subgroup.Commensurable

Definitions

Name	Category	Theorems
commensurator 📖	CompOp	2 math math: commensurator_mem_iff, eq
commensurator' 📖	CompOp	1 math math: commensurator'_mem_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comm 📖	mathematical	—	Subgroup.Commensurable	—	—
commensurable_conj 📖	mathematical	—	Subgroup.Commensurable ConjAct Subgroup SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid ConjAct.instDivInvMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Subgroup.pointwiseMulAction ConjAct.instMulDistribMulAction	—	not_iff_not Nat.card_congr
commensurable_inv 📖	mathematical	—	Subgroup.Commensurable ConjAct Subgroup SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid ConjAct.instDivInvMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Subgroup.pointwiseMulAction ConjAct.instMulDistribMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid ConjAct.instGroup	—	commensurable_conj inv_smul_smul
commensurator'_mem_iff 📖	mathematical	—	ConjAct Subgroup ConjAct.instGroup SetLike.instMembership Subgroup.instSetLike commensurator' Subgroup.Commensurable SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid ConjAct.instDivInvMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Subgroup.pointwiseMulAction ConjAct.instMulDistribMulAction	—	—
commensurator_mem_iff 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike commensurator Subgroup.Commensurable ConjAct SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid ConjAct.instDivInvMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Subgroup.pointwiseMulAction ConjAct.instMulDistribMulAction DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass EquivLike.toFunLike MulEquiv.instEquivLike ConjAct.toConjAct	—	—
conj 📖	mathematical	Subgroup.Commensurable	ConjAct Subgroup SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid ConjAct.instDivInvMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Subgroup.pointwiseMulAction ConjAct.instMulDistribMulAction	—	commensurable_conj
eq 📖	mathematical	Subgroup.Commensurable	commensurator	—	Subgroup.ext commensurable_conj trans symm
equivalence 📖	mathematical	—	Subgroup Subgroup.Commensurable	—	refl symm trans
refl 📖	mathematical	—	Subgroup.Commensurable	—	Subgroup.relIndex_self
trans 📖	—	Subgroup.Commensurable	—	—	Subgroup.relIndex_ne_zero_trans

(root)

Definitions

Name	Category	Theorems
Commensurable 📖	MathDef	—

---

← Back to Index