Theorem: MvPolynomial.degreeOf_C_mul (FormalSnarksProject/ToMathlib/ForTransformations.lean)

State before:
F : Type
inst✝¹ : Field F
σ R : Type
inst✝ : Field R
j : σ
c : R
hc : c ≠ 0
f : MvPolynomial σ R
⊢ degreeOf j (C c * f) = degreeOf j f
Tactic:
rw [Nat.eq_iff_le_and_ge]
State after:
F : Type
inst✝¹ : Field F
σ R : Type
inst✝ : Field R
j : σ
c : R
hc : c ≠ 0
f : MvPolynomial σ R
⊢ degreeOf j (C c * f) ≤ degreeOf j f ∧ degreeOf j f ≤ degreeOf j (C c * f)

State before:
F : Type
inst✝¹ : Field F
σ R : Type
inst✝ : Field R
j : σ
c : R
hc : c ≠ 0
f : MvPolynomial σ R
⊢ degreeOf j (C c * f) ≤ degreeOf j f ∧ degreeOf j f ≤ degreeOf j (C c * f)
Tactic:
constructor
State after:
case left
F : Type
inst✝¹ : Field F
σ R : Type
inst✝ : Field R
j : σ
c : R
hc : c ≠ 0
f : MvPolynomial σ R
⊢ degreeOf j (C c * f) ≤ degreeOf j f

case right
F : Type
inst✝¹ : Field F
σ R : Type
inst✝ : Field R
j : σ
c : R
hc : c ≠ 0
f : MvPolynomial σ R
⊢ degreeOf j f ≤ degreeOf j (C c * f)

State before:
case left
F : Type
inst✝¹ : Field F
σ R : Type
inst✝ : Field R
j : σ
c : R
hc : c ≠ 0
f : MvPolynomial σ R
⊢ degreeOf j (C c * f) ≤ degreeOf j f
Tactic:
convert MvPolynomial.degreeOf_C_mul_le f j c
State after:
no goals

State before:
case right
F : Type
inst✝¹ : Field F
σ R : Type
inst✝ : Field R
j : σ
c : R
hc : c ≠ 0
f : MvPolynomial σ R
⊢ degreeOf j f ≤ degreeOf j (C c * f)
Tactic:
have := MvPolynomial.degreeOf_C_mul_le (C (c) * f) j (1/c)
State after:
case right
F : Type
inst✝¹ : Field F
σ R : Type
inst✝ : Field R
j : σ
c : R
hc : c ≠ 0
f : MvPolynomial σ R
this : degreeOf j (C (1 / c) * (C c * f)) ≤ degreeOf j (C c * f)
⊢ degreeOf j f ≤ degreeOf j (C c * f)

State before:
case right
F : Type
inst✝¹ : Field F
σ R : Type
inst✝ : Field R
j : σ
c : R
hc : c ≠ 0
f : MvPolynomial σ R
this : degreeOf j (C (1 / c) * (C c * f)) ≤ degreeOf j (C c * f)
⊢ degreeOf j f ≤ degreeOf j (C c * f)
Tactic:
rw [<-mul_assoc] at this
State after:
case right
F : Type
inst✝¹ : Field F
σ R : Type
inst✝ : Field R
j : σ
c : R
hc : c ≠ 0
f : MvPolynomial σ R
this : degreeOf j (C (1 / c) * C c * f) ≤ degreeOf j (C c * f)
⊢ degreeOf j f ≤ degreeOf j (C c * f)

State before:
case right
F : Type
inst✝¹ : Field F
σ R : Type
inst✝ : Field R
j : σ
c : R
hc : c ≠ 0
f : MvPolynomial σ R
this : degreeOf j (C (1 / c) * C c * f) ≤ degreeOf j (C c * f)
⊢ degreeOf j f ≤ degreeOf j (C c * f)
Tactic:
rw [←C_mul] at this
State after:
case right
F : Type
inst✝¹ : Field F
σ R : Type
inst✝ : Field R
j : σ
c : R
hc : c ≠ 0
f : MvPolynomial σ R
this : degreeOf j (C (1 / c * c) * f) ≤ degreeOf j (C c * f)
⊢ degreeOf j f ≤ degreeOf j (C c * f)

State before:
case right
F : Type
inst✝¹ : Field F
σ R : Type
inst✝ : Field R
j : σ
c : R
hc : c ≠ 0
f : MvPolynomial σ R
this : degreeOf j (C (1 / c * c) * f) ≤ degreeOf j (C c * f)
⊢ degreeOf j f ≤ degreeOf j (C c * f)
Tactic:
simp only [one_div, ne_eq, hc, not_false_eq_true, inv_mul_cancel, map_one, one_mul] at this
State after:
case right
F : Type
inst✝¹ : Field F
σ R : Type
inst✝ : Field R
j : σ
c : R
hc : c ≠ 0
f : MvPolynomial σ R
this : degreeOf j f ≤ degreeOf j (C c * f)
⊢ degreeOf j f ≤ degreeOf j (C c * f)

State before:
case right
F : Type
inst✝¹ : Field F
σ R : Type
inst✝ : Field R
j : σ
c : R
hc : c ≠ 0
f : MvPolynomial σ R
this : degreeOf j f ≤ degreeOf j (C c * f)
⊢ degreeOf j f ≤ degreeOf j (C c * f)
Tactic:
convert this
State after:
no goals