Theorems · Theorem · commutative algebra

Ideal.IsMaximal.map_of_surjective_of_ker_le

∀ {R : Type u_1} {S : Type u_2} {F : Type u_3} [inst : Ring R] [inst_1 : Ring S] [inst_2 : FunLike F R S]
  [rc : RingHomClass F R S] {f : F},
  Function.Surjective ⇑f → ∀ {m : Ideal R} [m.IsMaximal], RingHom.ker f ≤ m → (Ideal.map f m).IsMaximal

Defined in

Mathlib.RingTheory.Ideal.Maps

Cited by

1 results in Mathlib

Foundations

Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingRingFunLikeRingHomClassIdeal.IsMaximal