English
Cancels(-u) (unitsSMul φ u w) is true exactly when Cancels u w is false; i.e., negating the unit flips the Cancels predicate.
Русский
Cancels(-u) (unitsSMul φ u w) истинно тогда и только тогда, когда Cancels u w ложно; инволюция меняет предикат отмены.
LaTeX
$$$\\mathrm{Cancels}(-u, \\mathrm{unitsSMul}(\\varphi,u,w)) \\; \\Leftrightarrow \\; \\lnot \\mathrm{Cancels}(u,w).$$$
Lean4
/-- A condition for not cancelling whose hypotheses are the same as those of the `cons` function. -/
theorem not_cancels_of_cons_hyp (u : ℤˣ) (w : NormalWord d)
(h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u') : ¬Cancels u w :=
by
simp only [Cancels, Option.map_eq_some_iff, Prod.exists, exists_and_right, exists_eq_right, not_and, not_exists]
intro hw x hx
rw [hx] at h2
simpa using h2 (-u) rfl hw
