Structures · Algebra
NonUnitalRingHomClass
NonUnitalRingHomClass F α β states that F is a type of non-unital (semi)ring
homomorphisms. You should extend this class when you extend NonUnitalRingHom.
- Defined in
- Mathlib.Algebra.Ring.Hom.Defs
- Shape
- 3 explicit arguments
Extends2
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- NonUnitalStarRingHom
- NonUnitalRingHom
How is a type an instance?
Loading the hierarchy index…
Assumed by129
- NonUnitalRingHomClass.toNonUnitalRingHom
- RingEquiv.ofBijective
- NonUnitalSubsemiring.map
- NonUnitalSubring.map
- NonUnitalRingHom.srange
- NonUnitalSubring.comap
- NonUnitalSubsemiring.comap
- Matrix.map_mul
- NonUnitalSubring.gc_map_comap
- NonUnitalSubsemiring.gc_map_comap
- DirectLimit.NonUnitalStarRing.of
- DirectLimit.NonUnitalRing.of
- TwoSidedIdeal.ker
- TwoSidedIdeal.comap
- NonUnitalRingHom.mem_srange
- DirectLimit.NonUnitalStarRing.lift
- DirectLimit.NonUnitalRing.lift
- NonUnitalRingHom.coe_srange
- SeminormedRing.induced
- IsQuasiregular.map
- RingEquiv.sofLeftInverse'
- StarRingEquiv.ofBijective
- NonUnitalRingHom.srangeRestrict
- StarRingEquiv.ofStarRingHom
- TwoSidedIdeal.ker_eq_bot
- NonUnitalRingHom.srange_eq_top_of_surjective
- NonUnitalSubring.mem_comap
- NonUnitalSubsemiring.map_le_iff_le_comap
- NonUnitalRingHom.srange_eq_top_iff_surjective
- NonUnitalSubsemiring.mem_comap
- DirectLimit.NonUnitalRing.hom_ext
- NonUnitalSubsemiring.equivMapOfInjective
- NonUnitalSubsemiring.comap_top
- NonUnitalSubring.map_le_iff_le_comap
- NonUnitalRingHom.srange_eq_map
- TwoSidedIdeal.mem_ker
- NonUnitalSubsemiring.map_map
- TwoSidedIdeal.ker_ringCon
- NonUnitalSubsemiring.map.congr_simp
- NonUnitalRingHom.eqOn_sclosure
- NonUnitalRingHom.eqSlocus
- NonUnitalSubring.equivMapOfInjective
- DirectLimit.NonUnitalRing.of_apply
- NonUnitalSubsemiring.mem_map
- NonUnitalStarRingHomClass.toNonUnitalStarRingHom
- DirectLimit.NonUnitalStarRing.hom_ext
- NonUnitalSubring.map.congr_simp
- DirectLimit.instStarRingOfStarHomClass
- DirectLimit.NonUnitalStarRing.hom_ext_iff
- NonUnitalSubsemiring.comap.congr_simp