Invariant

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

Statistics

Metric	Count
Definitions IsInvariantSubring, subtypeHom, toMulSemiringAction, Invariant	4
Theorems coe_subtypeHom, coe_subtypeHom', smul_mem	3
Total	7

IsInvariantSubring

Definitions

Name	Category	Theorems
subtypeHom 📖	CompOp	2 math math: coe_subtypeHom', coe_subtypeHom
toMulSemiringAction 📖	CompOp	2 math math: coe_subtypeHom', coe_subtypeHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_subtypeHom 📖	mathematical	—	DFunLike.coe MulSemiringActionHom MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass Subring SetLike.instMembership Subring.instSetLike Ring.toSemiring Subring.toRing toMulSemiringAction MulSemiringActionHom.instFunLike subtypeHom	—	—
coe_subtypeHom' 📖	mathematical	—	RingHomClass.toRingHom MulSemiringActionHom MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass Subring SetLike.instMembership Subring.instSetLike Ring.toSemiring Subring.toRing toMulSemiringAction MulSemiringActionHom.instFunLike Semiring.toNonAssocSemiring MulSemiringActionSemiHomClass.toRingHomClass DFunLike.coe MonoidHom MonoidHom.instFunLike MulSemiringAction.toDistribMulAction MulSemiringActionHom.instMulSemiringActionSemiHomClassCoeMonoidHom subtypeHom Subring.subtype	—	MulSemiringActionSemiHomClass.toRingHomClass MulSemiringActionHom.instMulSemiringActionSemiHomClassCoeMonoidHom
smul_mem 📖	mathematical	Subring SetLike.instMembership Subring.instSetLike	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction Ring.toSemiring	—	—

ProbabilityTheory.Kernel

Definitions

Name	Category	Theorems
Invariant 📖	MathDef	1 math math: IsReversible.invariant

(root)

Definitions

Name	Category	Theorems
IsInvariantSubring 📖	CompData	1 math math: instIsInvariantSubringOfIsInvariantSubfield

---

← Back to Index