piCongrRight_refl — Mathlib

English

The piCongrRight construction with identity on each component is the same as the identity AlgEquiv.

Русский

Конструкция piCongrRight с тождественными компонентами равна тождественному AlgEquiv.

LaTeX

$$$ (\\piCongrRight (\\lambda i, \\mathrm{AlgEquiv.refl})) = \\mathrm{AlgEquiv.refl} $$$

Lean4

@[simp]
theorem piCongrRight_refl : (piCongrRight fun i ↦ (AlgEquiv.refl : A₁ i ≃ₐ[R] A₁ i)) = AlgEquiv.refl :=
  rfl

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