Theorems · Definition · commutative algebra

Ideal.under

(A : Type u_2) → [inst : CommSemiring A] → {B : Type u_3} → [inst_1 : Semiring B] → [Algebra A B] → Ideal B → Ideal A

The ideal obtained by pulling back the ideal P from B to A.

Defined in

Mathlib.RingTheory.Ideal.Over

Cited by

170 results in Mathlib

Foundations

Depth 18 from the axioms, rests on 212 definitions · uses propext

Assumes

CommSemiringSemiringAlgebra