domLCongr_symm — Mathlib

English

The symmetry of domLCongr corresponds to applying the symmetric linear equivalence on the domain side.

Русский

Симметрия domLCongr соответствует применению симметричного линейного эквивалента по стороне домена.

LaTeX

$$domLCongr(R,N,ι,S e).symm = domLCongr(R,N,ι,S e.symm)$$

Lean4

@[simp]
theorem domLCongr_symm (e : M ≃ₗ[R] M₂) : (domLCongr R N ι S e).symm = domLCongr R N ι S e.symm :=
  rfl

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