Theorems · Theorem · commutative algebra
RingHom.IsIntegralElem.map
∀ {R : Type u_1} {S : Type u_2} {T : Type u_4} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Ring T] {f : R →+* S}
{x : S}, f.IsIntegralElem x → ∀ (g : S →+* T), (g.comp f).IsIntegralElem (g x)- Cited by
- 4 results in Mathlib
- Foundations
- Depth 111 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- RingHomstatement and proof · cited by 10,189
- Ringstatement and proof · cited by 7,463
- Polynomialproof · cited by 5,681
- map_zeroproof · cited by 1,614
- RingHom.compstatement · cited by 899
- Polynomial.Monicproof · cited by 461
- Polynomial.eval₂proof · cited by 267
- RingHom.IsIntegralElemstatement and proof · cited by 33
- Polynomial.eval₂_eq_eval_mapproof · cited by 29
Cited by4
Results whose statement or proof uses this declaration.
- IsIntegral.mapproof · cited by 22
- RingHom.IsIntegralElem.map_iffproof · cited by 1
- MvPolynomial.isIntegral_iff_isIntegral_coeffproof · cited by 1
- TensorProduct.toIntegralClosure_bijective_of_isLocalizationproof · cited by 0