fromCoset_eq_of_mem_range — Mathlib

English

If b ∈ f.hom.range, then fromCoset ⟨b • range, b, rfl⟩ = fromCoset ⟨range, 1, one_leftCoset _⟩.

Русский

Если b ∈ образ f.hom, то fromCoset(⟨b • range, b, rfl⟩) = fromCoset(⟨range, 1, one_leftCoset _⟩).

LaTeX

$$$ \text{If } b \in f.\mathrm{hom}.\mathrm{range},\; \mathrm{fromCoset}\langle b \cdot \uparrow f.\mathrm{hom}.\mathrm{range}, b, rfl\rangle = \mathrm{fromCoset}\langle f.\mathrm{hom}.\mathrm{range}, 1, \text{one_leftCoset } \_\rangle $$$

Lean4

theorem fromCoset_eq_of_mem_range {b : B} (hb : b ∈ f.hom.range) :
    fromCoset ⟨b • ↑f.hom.range, b, rfl⟩ = fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩ :=
  by
  congr
  nth_rw 2 [show (f.hom.range : Set B) = (1 : B) • f.hom.range from (one_leftCoset _).symm]
  rw [leftCoset_eq_iff, mul_one]
  exact Subgroup.inv_mem _ hb

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