Theorem: polynomial.remainder_in_ideal (Diploma/Polynomials/Division.lean)

State before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible quotient remainder : Polynomial n ord
dividers : List (Polynomial n ord)
div_sum_r_eq_p : divisible = quotient + remainder
quotient_in_ideal : quotient ∈ asIdeal dividers
⊢ divisible ∈ asIdeal dividers → remainder ∈ asIdeal dividers
Tactic:
intros divisible_in_ideal
State after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible quotient remainder : Polynomial n ord
dividers : List (Polynomial n ord)
div_sum_r_eq_p : divisible = quotient + remainder
quotient_in_ideal : quotient ∈ asIdeal dividers
divisible_in_ideal : divisible ∈ asIdeal dividers
⊢ remainder ∈ asIdeal dividers

State before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible quotient remainder : Polynomial n ord
dividers : List (Polynomial n ord)
div_sum_r_eq_p : divisible = quotient + remainder
quotient_in_ideal : quotient ∈ asIdeal dividers
divisible_in_ideal : divisible ∈ asIdeal dividers
⊢ remainder ∈ asIdeal dividers
Tactic:
have r_eq: remainder = divisible - quotient
State after:
case r_eq
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible quotient remainder : Polynomial n ord
dividers : List (Polynomial n ord)
div_sum_r_eq_p : divisible = quotient + remainder
quotient_in_ideal : quotient ∈ asIdeal dividers
divisible_in_ideal : divisible ∈ asIdeal dividers
⊢ remainder = divisible - quotient

n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible quotient remainder : Polynomial n ord
dividers : List (Polynomial n ord)
div_sum_r_eq_p : divisible = quotient + remainder
quotient_in_ideal : quotient ∈ asIdeal dividers
divisible_in_ideal : divisible ∈ asIdeal dividers
r_eq : remainder = divisible - quotient
⊢ remainder ∈ asIdeal dividers

State before:
case r_eq
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible quotient remainder : Polynomial n ord
dividers : List (Polynomial n ord)
div_sum_r_eq_p : divisible = quotient + remainder
quotient_in_ideal : quotient ∈ asIdeal dividers
divisible_in_ideal : divisible ∈ asIdeal dividers
⊢ remainder = divisible - quotient

n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible quotient remainder : Polynomial n ord
dividers : List (Polynomial n ord)
div_sum_r_eq_p : divisible = quotient + remainder
quotient_in_ideal : quotient ∈ asIdeal dividers
divisible_in_ideal : divisible ∈ asIdeal dividers
r_eq : remainder = divisible - quotient
⊢ remainder ∈ asIdeal dividers
Tactic:
rw [div_sum_r_eq_p, add_comm, sub_eq_add_neg, add_assoc,
    add_comm, add_right_neg, zero_add]
State after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible quotient remainder : Polynomial n ord
dividers : List (Polynomial n ord)
div_sum_r_eq_p : divisible = quotient + remainder
quotient_in_ideal : quotient ∈ asIdeal dividers
divisible_in_ideal : divisible ∈ asIdeal dividers
r_eq : remainder = divisible - quotient
⊢ remainder ∈ asIdeal dividers

State before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible quotient remainder : Polynomial n ord
dividers : List (Polynomial n ord)
div_sum_r_eq_p : divisible = quotient + remainder
quotient_in_ideal : quotient ∈ asIdeal dividers
divisible_in_ideal : divisible ∈ asIdeal dividers
r_eq : remainder = divisible - quotient
⊢ remainder ∈ asIdeal dividers
Tactic:
rw [r_eq]
State after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible quotient remainder : Polynomial n ord
dividers : List (Polynomial n ord)
div_sum_r_eq_p : divisible = quotient + remainder
quotient_in_ideal : quotient ∈ asIdeal dividers
divisible_in_ideal : divisible ∈ asIdeal dividers
r_eq : remainder = divisible - quotient
⊢ divisible - quotient ∈ asIdeal dividers

State before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible quotient remainder : Polynomial n ord
dividers : List (Polynomial n ord)
div_sum_r_eq_p : divisible = quotient + remainder
quotient_in_ideal : quotient ∈ asIdeal dividers
divisible_in_ideal : divisible ∈ asIdeal dividers
r_eq : remainder = divisible - quotient
⊢ divisible - quotient ∈ asIdeal dividers
Tactic:
exact sub_mem divisible_in_ideal quotient_in_ideal
State after:
no goals