coe_equiv_fst_eq_one_iff_mem — Mathlib

English

The first coordinate is 1 if and only if the original g belongs to T and aligns with the coset condition.

Русский

Первая координата равна единице тогда и только тогда, когда исходный элемент g принадлежит T и удовлетворяет косет-условию.

LaTeX

$$$ ((hST.equiv g).fst) = 1 \iff g \in T \text{ under appropriate conditions} $$$

Lean4

theorem coe_equiv_fst_eq_one_iff_mem {g : G} (h1 : 1 ∈ S) : ((hST.equiv g).fst : G) = 1 ↔ g ∈ T := by
  rw [equiv_fst_eq_mul_inv, mul_inv_eq_one, eq_comm, equiv_snd_eq_self_iff_mem _ h1]

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