Ideal

📁 Source: Mathlib/Algebra/TrivSqZeroExt/Ideal.lean

Statistics

Metric	Count
Definitions kerIdeal	1
Theorems kerIdeal_sq, mem_kerIdeal_iff_inr	2
Total	3

TrivSqZeroExt

Definitions

Name	Category	Theorems
kerIdeal 📖	CompOp	2 math math: kerIdeal_sq, mem_kerIdeal_iff_inr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
kerIdeal_sq 📖	mathematical	—	Ideal TrivSqZeroExt semiring CommSemiring.toSemiring IsScalarTower.to_smulCommClass MulOpposite MulOpposite.instSemiring MulOpposite.instAlgebra Algebra.id IsScalarTower.op_right SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul IsScalarTower.left DistribMulAction.toMulAction Monoid.toPow IdemSemiring.toSemiring Submodule.idemSemiring commSemiring kerIdeal Bot.bot Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	IsScalarTower.to_smulCommClass IsScalarTower.op_right IsScalarTower.left pow_two Ideal.mem_bot inr_mul_inr
mem_kerIdeal_iff_inr 📖	mathematical	—	TrivSqZeroExt Ideal semiring CommSemiring.toSemiring IsScalarTower.to_smulCommClass MulOpposite MulOpposite.instSemiring MulOpposite.instAlgebra Algebra.id IsScalarTower.op_right SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul IsScalarTower.left DistribMulAction.toMulAction SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule kerIdeal inr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass snd	—	IsScalarTower.to_smulCommClass IsScalarTower.op_right IsScalarTower.left fst_inr

---

← Back to Index