Theorems · Theorem · ring theory
AddMonoidAlgebra.Monic.supDegree_mul_of_ne_zero_left
∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
{p q : AddMonoidAlgebra R A} {D : A → B} [inst_3 : AddZeroClass A] [inst_4 : Add B] [AddLeftStrictMono B]
[AddRightStrictMono B],
Function.Injective D →
(∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) →
AddMonoidAlgebra.Monic D q →
p ≠ 0 → AddMonoidAlgebra.supDegree D (p * q) = AddMonoidAlgebra.supDegree D p + AddMonoidAlgebra.supDegree D q- Defined in
- Mathlib.Algebra.MonoidAlgebra.Degree
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement and proof · cited by 13,802
- LinearOrderstatement and proof · cited by 8,572
- mul_oneproof · cited by 3,885
- Nontrivialproof · cited by 2,416
- AddZeroClassstatement and proof · cited by 1,237
- OrderBotstatement and proof · cited by 1,055
- AddMonoidAlgebrastatement and proof · cited by 649
- AddLeftStrictMonostatement and proof · cited by 203
- subsingleton_or_nontrivialproof · cited by 161
- AddRightStrictMonostatement and proof · cited by 160
- AddMonoidAlgebra.supDegreestatement · cited by 49
- AddMonoidAlgebra.leadingCoeffproof · cited by 23
Cited by4
Results whose statement or proof uses this declaration.
- MvPolynomial.supDegree_esymmAlgHomMonomialproof · cited by 2
- AddMonoidAlgebra.Monic.leadingCoeff_mul_eq_leftproof · cited by 2
- AddMonoidAlgebra.Monic.supDegree_powproof · cited by 1
- AddMonoidAlgebra.Monic.supDegree_mulproof · cited by 0