The meta properties of integral ring homomorphisms. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
theorem
ring_hom.is_integral_stable_under_composition
:
ring_hom.stable_under_composition (λ (R S : Type u_1) (_x : comm_ring R) (_x_1 : comm_ring S) (f : R →+* S), f.is_integral)
theorem
ring_hom.is_integral_respects_iso
:
ring_hom.respects_iso (λ (R S : Type u_1) (_x : comm_ring R) (_x_1 : comm_ring S) (f : R →+* S), f.is_integral)
theorem
ring_hom.is_integral_stable_under_base_change
:
ring_hom.stable_under_base_change (λ (R S : Type u_1) (_x : comm_ring R) (_x_1 : comm_ring S) (f : R →+* S), f.is_integral)