piCongrRight_symm — Mathlib

English

The symmetry of piCongrRight is computed componentwise by taking the componentwise inverses.

Русский

Симметрия piCongrRight вычисляется по координатам через <<обратные>> компонент.

LaTeX

$$$ (\\mathrm{piCongrRight}\\, e).symm = \\mathrm{piCongrRight}\\, (i \\mapsto (e(i)).symm) $$$

Lean4

@[simp]
theorem piCongrRight_symm (e : ∀ i, A₁ i ≃ₐ[R] A₂ i) : (piCongrRight e).symm = piCongrRight fun i ↦ (e i).symm :=
  rfl

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