toSubgroupEquiv_neg_apply — Mathlib

English

If a ∈ toSubgroup A B u, then applying the negated isomorphism to the image of a under the positive isomorphism returns a.

Русский

Если a ∈ toSubgroup A B u, то применение обратного изоморфизма к изображению a через положительный изоморфизм возвращает a.

LaTeX

$$$\\forall a \\in toSubgroup A B u,\; (toSubgroupEquiv(φ,-u)(toSubgroupEquiv(φ,u)(a)) : G) = a$$$

Lean4

@[simp]
theorem toSubgroupEquiv_neg_apply (u : ℤˣ) (a : toSubgroup A B u) :
    (toSubgroupEquiv φ (-u) (toSubgroupEquiv φ u a) : G) = a :=
  by
  rcases Int.units_eq_one_or u with rfl | rfl
  · simp [toSubgroup]
  · simp only [toSubgroup_neg_one, toSubgroupEquiv_neg_one, SetLike.coe_eq_coe]
    exact φ.apply_symm_apply a

Похожие утверждения