Defs

📁 Source: Mathlib/RingTheory/Invariant/Defs.lean

Statistics

Metric	Count
Definitions IsInvariant	1
Theorems isInvariant, isInvariant_iff	2
Total	3

Algebra

Definitions

Name	Category	Theorems
IsInvariant 📖	CompData	5 math math: isInvariant_of_isGalois, isInvariant_iff, instIsInvariantSubtypeMemSubalgebraSubalgebraSubgroupQuotient, isInvariant_of_isGalois', IsGaloisGroup.isInvariant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isInvariant_iff 📖	mathematical	—	IsInvariant DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	—

Algebra.IsInvariant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isInvariant 📖	mathematical	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid MulSemiringAction.toDistribMulAction	DFunLike.coe RingHom CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	—

---

← Back to Index