congr_symm_apply_of — Mathlib

English

Symmetric congruence maps the inverse on the other side.

Русский

Симметричная конгруэнтность отображает обратно на другую сторону.

LaTeX

$$$(congr e he).symm (of G' i g) = of G f i ((e i)^{-1} g).$$$

Lean4

theorem congr_symm_apply_of (e : (i : ι) → G i ≃+* G' i)
    (he : ∀ i j h, (e j).toRingHom.comp (f i j h) = (f' i j h).comp (e i)) {i : ι} (g : G' i) :
    (congr e he).symm (of G' _ i g) = of G (fun _ _ h ↦ f _ _ h) i ((e i).symm g) := by
  simp only [congr, RingEquiv.ofRingHom_symm_apply, map_apply_of, RingHom.coe_coe]

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