IdempotentFG

Statistics

Metric	Count
Definitions	0
Theorems `isIdempotentElem_iff_eq_bot_or_top`, `isIdempotentElem_iff_of_fg`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`isIdempotentElem_iff_eq_bot_or_top` 📖	mathematical	`FG` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`IsIdempotentElem` `Ideal` `Submodule.mul` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Bot.bot` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Top.top` `Submodule.instTop`	—	`IsScalarTower.right` `isIdempotentElem_iff_of_fg` `span_singleton_one` `IsIdempotentElem.iff_eq_zero_or_one` `IsCancelMulZero.toIsLeftCancelMulZero` `IsDomain.toIsCancelMulZero` `Submodule.mul_bot` `mul_top` `instIsTwoSided_1`
`isIdempotentElem_iff_of_fg` 📖	mathematical	`FG` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`IsIdempotentElem` `Ideal` `Submodule.mul` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Submodule.span` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Set` `Set.instSingletonSet`	—	`IsScalarTower.right` `Submodule.exists_mem_and_smul_eq_self_of_fg_of_le_smul` `IsScalarTower.left` `smul_eq_mul` `Eq.ge` `antisymm` `instAntisymmLe` `mem_span_singleton'` `mul_comm` `Submodule.span_singleton_le_iff_mem` `span_singleton_mul_span_singleton` `instIsTwoSided_1` `IsIdempotentElem.eq`

---