## Stream: new members

### Topic: How to rewrite (0 : nat) as bot, or conversely

#### Antoine Chambert-Loir (Mar 18 2023 at 11:17):

Yesterday, I had to change 0 : nat into ⊥ : nat in some equality h : … = 0.
In the absence of nat.zero_eq_bot, there does not seem to be a preferred way to do that.
I had entered change : _ = ⊥, but I finally decided I prefered adding have : (0 : nat) = ⊥ := rfl.
Which one is preferable?

Below is a MWE where @María Inés de Frutos Fernández and I use this.

import data.mv_polynomial.variables

variables {σ : Type*} {R : Type*} [comm_semiring R]

namespace mv_polynomial

lemma total_degree_eq_zero_iff (p : mv_polynomial σ R) :
p.total_degree = 0
↔ ∀ (m : σ →₀ ℕ) (hm : m ∈ p.support) (x : σ), m x = 0 :=
begin
have nat_zero_eq_bot : (0 : ℕ) = ⊥ := rfl,
rw [nat_zero_eq_bot, total_degree, finset.sup_eq_bot_iff, ← nat_zero_eq_bot],
apply forall_congr,
intro a,
apply forall_congr,
intro ha,
simp only [finsupp.sum, finset.sum_eq_zero_iff, finsupp.mem_support_iff, not_imp_self],
end

end mv_polynomial


docs#bot_eq_zero

#### Antoine Chambert-Loir (Mar 18 2023 at 12:36):

Thanks! I don't understand how I didn't find it - probably because I was looking to zero_eq_bot

#### Adam Topaz (Mar 18 2023 at 12:48):

Another option is to introduce the term on the fly and rewrite like this rw (show 0 = \bot, from rfl)

Last updated: Dec 20 2023 at 11:08 UTC