Theorems · Theorem · ring theory

AddMonoidAlgebra.leadingCoeff.congr_simp

∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  (D D_1 : A → B),
  D = D_1 →
    ∀ [inst_3 : Nonempty A] (f f_1 : AddMonoidAlgebra R A),
      f = f_1 → AddMonoidAlgebra.leadingCoeff D f = AddMonoidAlgebra.leadingCoeff D_1 f_1

Defined in: Mathlib.Algebra.MonoidAlgebra.Degree
Cited by: 2 results in Mathlib
Foundations: Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Semiring LinearOrder OrderBot Nonempty

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites5

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
OrderBotstatement and proof · cited by 1,055
AddMonoidAlgebrastatement and proof · cited by 649
AddMonoidAlgebra.leadingCoeffstatement and proof · cited by 23

Cited by2

Results whose statement or proof uses this declaration.

AddMonoidAlgebra.Monic.ne_zeroproof · cited by 4
AddMonoidAlgebra.leadingCoeff_mulproof · cited by 0