Structures · Algebra
Ideal.IsTwoSided
A left ideal I : Ideal R is two-sided if it is also a right ideal.
- Defined in
- Mathlib.RingTheory.Ideal.Defs
- Shape
- One type argument · adds mul_mem_of_left
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by216
- Ideal.Quotient.mk_surjective
- Ideal.Quotient.mkₐ
- Ideal.Quotient.eq_zero_iff_mem
- Ideal.mul_mem_right
- Ideal.mk_ker
- Ideal.mul_top
- Ideal.Quotient.factor
- Ideal.quotientMap
- Ideal.quotientEquivAlgOfEq
- Ideal.Quotient.eq
- Ideal.Quotient.factorₐ
- Ideal.span_singleton_pow
- Ideal.mul_le_left
- Ideal.Quotient.lift
- Ideal.Quotient.factorPow
- Ideal.Quotient.ringHom_ext
- Ideal.quotEquivOfEq
- Ideal.Quotient.liftₐ
- Ideal.map_quotient_self
- Ideal.span_singleton_mul_span_singleton
- Ideal.quotientMapₐ
- Ideal.mul_le_inf
- Ideal.Quotient.lift_mk
- Ideal.quotientMap_mk
- Ideal.IsPrime.mul_mem_iff_mem_or_mem
- Ideal.Quotient.mk_eq_mk_iff_sub_mem
- Ideal.Quotient.mk_eq_mk
- Ideal.quotientEquivAlg
- Submodule.colon_univ
- Ideal.quotientEquiv
- Ideal.quotientInfToPiQuotient
- Ideal.toTwoSided
- Ideal.Quotient.algHom_ext
- Ideal.Quotient.lift_surjective_of_surjective
- Ideal.Quotient.mkₐ_surjective
- Ideal.Quotient.factor_eq
- Ideal.span_mul_span
- Ideal.Quotient.factor_comp_apply
- Ideal.Quotient.mk_out
- Ideal.Quotient.mkₐ_ker
- Ideal.comap_map_quotientMk
- Ideal.sup_iInf_eq_top
- Ideal.algebraMap_quotient_injective
- Ideal.Quotient.algebraQuotientOfLEComap
- Ideal.sup_mul_eq_of_coprime_left
- Ideal.span_mul_span'
- Ideal.IsPrime.mul_mem_left_iff
- Ideal.Quotient.factor_surjective
- Submodule.span_smul_span
- Ideal.Quotient.mk_algebraMap
Ancestors0
No ancestors.