congr_refl_refl — Mathlib

English

The congruence of identity maps on M and N is the identity on the tensor product: congr Refl(R,M) Refl(R,N) = Refl(R, TensorProduct R M N).

Русский

Сопоставление тождества на M и на N даёт тождественное отображение на произведение: congr_refl_refl = refl на TensorProduct.

LaTeX

$$$ congr\\ (\\mathrm{refl}\\ R\\ M)\\ (\\mathrm{refl}\\ R\\ N) = \\mathrm{refl}\\ R\\ (TensorProduct\\ R\\ M\\ N) $$$

Lean4

@[simp]
theorem congr_refl_refl : congr (.refl R M) (.refl R N) = .refl R _ :=
  LinearEquiv.toLinearMap_injective <| ext' fun _ _ ↦ rfl

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