piCongrLeft'_symm — Mathlib

English

The left pi-congruence is compatible with taking symmetries: the inverse of piCongrLeft' is piCongrLeft' with the index equivalence inverted.

Русский

Левая pi-конгруэнтность совместима с взятием симметрии: обратное к piCongrLeft' равно piCongrLeft' с инверсией индексного эквивалентного отображения.

LaTeX

$$$$ \\big(\\text{piCongrLeft'}(R)\\ e\\big)^{-1} = \\text{piCongrLeft'}(R)\\ e^{-1}. $$$$

Lean4

@[simp]
theorem piCongrLeft'_symm {R : Type*} [NonUnitalNonAssocSemiring R] (e : α ≃ β) :
    (RingEquiv.piCongrLeft' (fun _ => R) e).symm = RingEquiv.piCongrLeft' _ e.symm := by
  simp only [piCongrLeft', RingEquiv.symm, MulEquiv.symm, Equiv.piCongrLeft'_symm]

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