Group

📁 Source: Mathlib/Algebra/Ring/Action/Group.lean

Statistics

Metric	Count
Definitions toRingEquiv	1
Theorems toRingEquiv_apply, toRingEquiv_symm_apply	2
Total	3

MulSemiringAction

Definitions

Name	Category	Theorems
toRingEquiv 📖	CompOp	6 math math: toRingEquiv_apply, toRingAut_apply, toAlgEquiv_toEquiv, toRingEquiv_symm_apply, Unitary.toRingEquiv_conjStarAlgAut, toRingEquiv_algEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toRingEquiv_apply 📖	mathematical	—	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike toRingEquiv SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid toDistribMulAction	—	—
toRingEquiv_symm_apply 📖	mathematical	—	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm toRingEquiv SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction DistribMulAction.toMulAction AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne toDistribMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—

---

← Back to Index