Theorems · Theorem · commutative algebra
Ideal.comap_symm
∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {I : Ideal R} (f : R ≃+* S),
Ideal.comap f.symm I = Ideal.map f IIf f : R ≃+* S is a ring isomorphism and I : Ideal R, then comap f.symm I = map f I.
- Defined in
- Mathlib.RingTheory.Ideal.Maps
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 29 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement and proof · cited by 13,802
- Idealstatement and proof · cited by 4,748
- RingEquivstatement and proof · cited by 1,147
- Ideal.mapstatement · cited by 692
- RingEquiv.symmstatement · cited by 567
- Ideal.comapstatement · cited by 443
- Ideal.map_comap_of_equivproof · cited by 6
Cited by12
Results whose statement or proof uses this declaration.
- Ideal.pointwise_smul_eq_comapproof · cited by 5
- Algebra.WeaklyQuasiFiniteAt.baseChangeproof · cited by 2
- Ideal.inertiaDeg_smulproof · cited by 2
- RingHom.FinitePresentation.polynomial_inductionproof · cited by 1
- IsArithFrobAt.conjproof · cited by 1
- Ideal.apply_mem_of_equiv_iffproof · cited by 1
- RingEquiv.height_mapproof · cited by 0
- Algebra.IsFiniteSplit.bijective_algebraMap_quotientproof · cited by 0
- Ideal.LiesOver.of_eq_map_equivproof · cited by 0
- Algebra.Presentation.span_range_relation_eq_ker_baseChangeproof · cited by 0
- Ring.DimensionLEOne.of_ringEquivproof · cited by 0
- Ideal.symm_apply_mem_of_equiv_iffproof · cited by 0