Theorems · Theorem · commutative algebra

MvPolynomial.IsHomogeneous.sub

∀ {R : Type u_5} {σ : Type u_6} [inst : CommRing R] {φ ψ : MvPolynomial σ R} {n : ℕ},
  φ.IsHomogeneous n → ψ.IsHomogeneous n → (φ - ψ).IsHomogeneous n

Defined in: Mathlib.RingTheory.MvPolynomial.Homogeneous
Cited by: 2 results in Mathlib
Foundations: Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CommRingstatement and proof · cited by 17,173
Finsuppstatement · cited by 5,255
MvPolynomialstatement and proof · cited by 2,140
MvPolynomial.IsHomogeneousstatement and proof · cited by 68
Submodule.sub_memproof · cited by 43
MvPolynomial.homogeneousSubmoduleproof · cited by 23

Cited by2

Results whose statement or proof uses this declaration.

WeierstrassCurve.isHomogeneous_addSubMapproof · cited by 1
MvPolynomial.IsHomogeneous.funext_of_le_cardproof · cited by 1