English
A variant form of the equivalence Cancels(-u)(unitsSMul φ u w) ↔ ¬Cancels u w, specialized with an auxiliary equality; the statement ties into the equality cases in the cancellation analysis.
Русский
Вариант эквивалентности Cancels(-u)(unitsSMul φ u w) ⇔ ¬Cancels u w, специфицируемый дополнительным равенством; связано с случаями отмены в анализе.
LaTeX
$$$\\mathrm{Cancels}(-u, \\mathrm{unitsSMul}(\\varphi,u,w)) \\; \\Leftrightarrow \\; \\lnot \\mathrm{Cancels}(u,w) \\quad \\text{(with additional equality conditions).}$$$
Lean4
theorem unitsSMul_cancels_iff (u : ℤˣ) (w : NormalWord d) : Cancels (-u) (unitsSMul φ u w) ↔ ¬Cancels u w :=
by
by_cases h : Cancels u w
· simp only [unitsSMul, h, dite_true, not_true_eq_false, iff_false]
induction w using consRecOn with
| ofGroup => simp [Cancels, unitsSMulWithCancel]
| cons g u' w h1 h2 _ =>
intro hc
apply not_cancels_of_cons_hyp _ _ h2
simp only [Cancels, cons_head, cons_toList, List.head?_cons, Option.map_some, Option.some.injEq] at h
cases h.2
simpa [Cancels, unitsSMulWithCancel, Subgroup.mul_mem_cancel_left] using hc
· simp only [unitsSMul, dif_neg h]
simpa [Cancels] using h
