Theorems · Theorem · commutative algebra

comap_prime

∀ {M : Type u_1} {N : Type u_2} [inst : CommMonoidWithZero M] [inst_1 : CommMonoidWithZero N] {F : Type u_3}
  {G : Type u_4} [inst_2 : FunLike F M N] [MonoidWithZeroHomClass F M N] [inst_4 : FunLike G N M] [MulHomClass G N M]
  (f : F) (g : G) {p : M}, (∀ (a : M), g (f a) = a) → Prime (f p) → Prime p

Defined in

Mathlib.Algebra.Prime.Lemmas

Cited by

3 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext

Assumes

CommMonoidWithZeroCommMonoidWithZeroFunLikeMonoidWithZeroHomClassFunLikeMulHomClass