Theorems · Theorem · commutative algebra

AddMonoidAlgebra.support_coeff_divOf

∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCommMonoid G] [inst_2 : IsCancelAdd G] (g : G)
  (x : AddMonoidAlgebra k G), (x.divOf g).coeff.support = x.coeff.support.preimage (fun x => g + x) ⋯

Defined in

Mathlib.Algebra.MonoidAlgebra.Division

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidIsCancelAdd