Theorems · Definition · commutative algebra
Subring.comap
{R : Type u} → {S : Type v} → [inst : NonAssocRing R] → [inst_1 : NonAssocRing S] → (R →+* S) → Subring S → Subring RThe preimage of a subring along a ring homomorphism is a subring.
- Defined in
- Mathlib.Algebra.Ring.Subring.Basic
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 23 from the axioms · uses propext
- Assumes
- NonAssocRingNonAssocRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- RingHomstatement and proof · cited by 10,189
- Set.preimageproof · cited by 4,946
- AddSubgroupproof · cited by 3,232
- Submonoidproof · cited by 3,086
- Subringstatement and proof · cited by 602
- NonAssocRingstatement and proof · cited by 483
- MonoidHomClass.toMonoidHomproof · cited by 294
- AddMonoidHomClass.toAddMonoidHomproof · cited by 232
- Submonoid.comapproof · cited by 179
- Subsemigroup.carrierproof · cited by 160
- Submonoid.toSubsemigroupproof · cited by 159
Cited by24
Results whose statement or proof uses this declaration.
- Subfield.comapproof · cited by 29
- Subring.gc_map_comapstatement · cited by 7
- Subring.mem_comapstatement · cited by 3
- ValuationSubring.comapproof · cited by 3
- Subring.map_le_iff_le_comapstatement · cited by 3
- Subring.comap_map_eqstatement and proof · cited by 1
- Subring.top_prodstatement · cited by 1
- CommRingCat.closure_range_union_range_eq_top_of_isPushoutproof · cited by 1
- Subring.map_comap_eqstatement and proof · cited by 1
- Subring.map_comap_eq_selfstatement and proof · cited by 1
- Subring.map_equiv_eq_comap_symmstatement and proof · cited by 1
- Subring.comap_map_eq_self_of_injectivestatement and proof · cited by 1