Structures · Algebra
RingEquivClass
RingEquivClass F R S states that F is a type of ring structure preserving equivalences.
You should extend this class when you extend RingEquiv.
- Defined in
- Mathlib.Algebra.Ring.Equiv
- Shape
- 3 explicit arguments · adds map_add
Extends1
Extended by4
Concrete types that are instances3
- RingEquiv
- OrderRingIso
- StarRingEquiv
How is a type an instance?
Loading the hierarchy index…
Assumed by23
- RingEquivClass.toRingEquiv
- isAlgebraic_ringHom_iff_of_comp_eq
- Ideal.map_comap_eq_self_of_equiv
- Algebra.isAlgebraic_ringHom_iff_of_comp_eq
- RingHom.ker_equiv
- Ideal.comap_isMaximal_of_equiv
- IsDiscreteValuationRing.RingEquivClass.isDiscreteValuationRing
- OrderRingIsoClass.toOrderRingIso
- RingEquivClass.toLinearEquivClassRat
- transcendental_ringHom_iff_of_comp_eq
- RingEquivClass.toMulEquivClass
- RingEquivClass.toRingEquiv.congr_simp
- RingEquivClass.toAddEquivClass
- RingEquiv.isStablyFiniteRing_iff
- RingEquivClass.toRingHomClass
- instCoeTCOrderRingIsoOfOrderIsoClassOfRingEquivClass
- RingEquivClass.map_add
- Ideal.mem_map_of_equiv
- RingEquivClass.toNonUnitalRingHomClass
- algebraicIndependent_ringHom_iff_of_comp_eq
- Ideal.map_isMaximal_of_equiv
- Ideal.map_isPrime_of_equiv
- Algebra.transcendental_ringHom_iff_of_comp_eq