Congr

📁 Source: Mathlib/RingTheory/SimpleRing/Congr.lean

Statistics

Metric	Count
Definitions	0
Theorems of_ringEquiv, of_surjective, isSimpleRing_iff_isTwoSided_imp	3
Total	3

IsSimpleRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_ringEquiv 📖	mathematical	—	IsSimpleRing	—	OrderIso.isSimpleOrder simple
of_surjective 📖	mathematical	DFunLike.coe RingHom NonAssocRing.toNonAssocSemiring RingHom.instFunLike	IsSimpleRing NonAssocRing.toNonUnitalNonAssocRing	—	OrderIso.isSimpleOrder simple RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass RingHom.injective

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSimpleRing_iff_isTwoSided_imp 📖	mathematical	—	IsSimpleRing NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Nontrivial Bot.bot Ideal Ring.toSemiring Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Top.top Submodule.instTop	—	Equiv.nontrivial_congr Equiv.forall_congr_left OrderIso.injective OrderIso.apply_symm_apply

---

← Back to Index