α : Type u
β : Type v
f : α → β
x y : FreeCommRing α
s✝ t : Set α
i✝ : ℤ
s : Set α
i : ℕ
hi : IsSupported (↑↑i) s
⊢ IsSupported (↑↑i + 1) s
α : Type u
β : Type v
f : α → β
x y : FreeCommRing α
s✝ t : Set α
i✝ : ℤ
s : Set α
i : ℕ
hi : IsSupported (↑↑i) s
⊢ IsSupported (↑(↑i + 1)) s
rw [Int.cast_add, Int.cast_one]
no goals
α : Type u
β : Type v
f : α → β
x y : FreeCommRing α
s✝ t : Set α
i✝ : ℤ
s : Set α
i : ℕ
hi : IsSupported (↑↑i) s
⊢ IsSupported (↑↑i + 1) s
exact isSupported_add hi isSupported_one
α : Type u
β : Type v
f : α → β
x y : FreeCommRing α
s✝ t : Set α
i✝ : ℤ
s : Set α
i : ℕ
hi : IsSupported (↑(-↑i)) s
⊢ IsSupported (↑(-↑i) - 1) s
α : Type u
β : Type v
f : α → β
x y : FreeCommRing α
s✝ t : Set α
i✝ : ℤ
s : Set α
i : ℕ
hi : IsSupported (↑(-↑i)) s
⊢ IsSupported (↑(-↑i - 1)) s
rw [Int.cast_sub, Int.cast_one]
no goals
α : Type u
β : Type v
f : α → β
x y : FreeCommRing α
s✝ t : Set α
i✝ : ℤ
s : Set α
i : ℕ
hi : IsSupported (↑(-↑i)) s
⊢ IsSupported (↑(-↑i) - 1) s
exact isSupported_sub hi isSupported_one