Skip to content

Commit 93994a0

Browse files
committed
chore(Algebra/Polynomial/Homogenize): fix typo in lemma name (leanprover-community#37725)
Rename the lemma `isHomogenous_toTupleMvPolynomial` to `isHomogeneous_toTupleMvPolynomial`. Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>
1 parent fea9737 commit 93994a0

1 file changed

Lines changed: 4 additions & 1 deletion

File tree

Mathlib/Algebra/Polynomial/Homogenize.lean

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -254,12 +254,15 @@ lemma toTupleMvPolynomial_one_eq (p : R[X]) :
254254
p.toTupleMvPolynomial 1 = (MvPolynomial.X 1) ^ p.natDegree :=
255255
rfl
256256

257-
lemma isHomogenous_toTupleMvPolynomial (p : R[X]) (i : Fin 2) :
257+
lemma isHomogeneous_toTupleMvPolynomial (p : R[X]) (i : Fin 2) :
258258
(p.toTupleMvPolynomial i).IsHomogeneous p.natDegree := by
259259
fin_cases i
260260
· simp [toTupleMvPolynomial]
261261
· simpa [toTupleMvPolynomial] using MvPolynomial.isHomogeneous_X_pow 1 p.natDegree
262262

263+
@[deprecated (since := "2026-04-06")]
264+
alias isHomogenous_toTupleMvPolynomial := isHomogeneous_toTupleMvPolynomial
265+
263266
lemma eval_X_toTupleMvPolynomial_zero_eq (p : R[X]) :
264267
MvPolynomial.aeval ![X, 1] (p.toTupleMvPolynomial 0) =
265268
p * MvPolynomial.aeval ![X, 1] (p.toTupleMvPolynomial 1) := by

0 commit comments

Comments
 (0)