Theorems · Theorem · ring theory
NonUnitalRingHom.map_range
∀ {R : Type u} {S : Type v} {T : Type u_1} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S]
[inst_2 : NonUnitalNonAssocRing T] (g : S →ₙ+* T) (f : R →ₙ+* S), NonUnitalSubring.map g f.range = (g.comp f).range- Cited by
- 0 results in Mathlib
- Foundations
- Depth 27 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Top.topproof · cited by 9,680
- NonUnitalNonAssocRingstatement and proof · cited by 354
- NonUnitalSubringstatement · cited by 185
- NonUnitalRingHomstatement and proof · cited by 157
- NonUnitalRingHom.compstatement and proof · cited by 38
- NonUnitalSubring.mapstatement and proof · cited by 19
- NonUnitalRingHom.rangestatement and proof · cited by 12
- NonUnitalSubring.map.congr_simpproof · cited by 1
- NonUnitalRingHom.range_eq_mapproof · cited by 1
- NonUnitalSubring.map_mapproof · cited by 1
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.