Theorems · Theorem · ring theory

AddMonoidAlgebra.Monic.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 : ℕ},
  (∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) →
    Function.Injective D → AddMonoidAlgebra.Monic D p → AddMonoidAlgebra.Monic D (p ^ n)

Defined in

Mathlib.Algebra.MonoidAlgebra.Degree

Cited by

3 results in Mathlib

Foundations

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

Assumes

SemiringAddMonoidAddMonoidLinearOrderOrderBotAddLeftStrictMonoAddRightStrictMono