Theorems · Theorem · ring theory

AddMonoidAlgebra.Monic.supDegree_pow

∀ {R : Type u_1} [inst : Semiring R] {A : Type u_8} {B : Type u_9} [inst_1 : AddMonoid A] [inst_2 : AddMonoid B]
  [inst_3 : LinearOrder B] [inst_4 : OrderBot B] [AddLeftStrictMono B] [AddRightStrictMono B] {D : A → B}
  {p : AddMonoidAlgebra R A} {n : ℕ},
  D 0 = 0 →
    (∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) →
      Function.Injective D →
        ∀ [Nontrivial R],
          AddMonoidAlgebra.Monic D p → AddMonoidAlgebra.supDegree D (p ^ n) = n • AddMonoidAlgebra.supDegree D p

Defined in

Mathlib.Algebra.MonoidAlgebra.Degree

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringAddMonoidAddMonoidLinearOrderOrderBotAddLeftStrictMonoAddRightStrictMonoNontrivial