Theorems · Theorem · commutative algebra

Ideal.under_smul

∀ (A : Type u_2) [inst : CommSemiring A] {B : Type u_3} [inst_1 : Semiring B] [inst_2 : Algebra A B] (P : Ideal B)
  {G : Type u_5} [inst_3 : Group G] [inst_4 : MulSemiringAction G B] (g : G) [SMulCommClass G A B],
  Ideal.under A (g • P) = Ideal.under A P

Defined in

Mathlib.RingTheory.Ideal.Over

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringAlgebraGroupMulSemiringActionSMulCommClass