Theorems · Definition · commutative algebra
RingHom.rangeRestrict
{R : Type u} → {S : Type v} → [inst : NonAssocRing R] → [inst_1 : NonAssocRing S] → (f : R →+* S) → R →+* ↥f.rangeRestriction of a ring homomorphism to its range interpreted as a subsemiring.
This is the bundled version of Set.rangeFactorization.
- Defined in
- Mathlib.Algebra.Ring.Subring.Basic
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NonAssocRingNonAssocRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- RingHomstatement and proof · cited by 10,189
- Subringstatement · cited by 602
- NonAssocRingstatement and proof · cited by 483
- RingHom.rangestatement and proof · cited by 138
- RingHom.codRestrictproof · cited by 12
Cited by15
Results whose statement or proof uses this declaration.
- HomogeneousLocalization.awayMapproof · cited by 27
- RingEquiv.ofLeftInverseproof · cited by 5
- RingHom.rangeRestrict_surjectivestatement and proof · cited by 3
- HomogeneousLocalization.val_awayMap_eq_auxproof · cited by 2
- RingHom.coe_rangeRestrictstatement · cited by 1
- IsGaloisGroup.finiteproof · cited by 1
- IsLocalRing.exists_factor_valuationRingproof · cited by 1
- AlgebraicGeometry.ValuativeCriterion.Existence.of_specializingMapproof · cited by 1
- Ideal.eq_zero_of_polynomial_mem_map_rangestatement and proof · cited by 1
- Polynomial.isJacobsonRing_polynomial_of_isJacobsonRingproof · cited by 1
- CommRingCat.essentiallySmall_of_localizationAwayproof · cited by 1
- bijective_rangeRestrict_comp_of_valuationRingstatement and proof · cited by 1