English
The product-congruent map acts componentwise: (e1.prodCongr e2) p = (e1 p.1, e2 p.2).
Русский
Отображение prodCongr действует по компонентам: p ↦ (e1 p.1, e2 p.2).
LaTeX
$$$(e_1.\mathrm{prodCongr} e_2) p = (e_1 p.1, e_2 p.2)$$$
Lean4
/-- Equivalence given by a block lower diagonal matrix. `e₁` and `e₂` are diagonal square blocks,
and `f` is a rectangular block below the diagonal. -/
protected def skewProd (f : M →ₗ[R] M₄) : (M × M₃) ≃ₗ[R] M₂ × M₄ :=
{
((e₁ : M →ₗ[R] M₂).comp (LinearMap.fst R M M₃)).prod
((e₂ : M₃ →ₗ[R] M₄).comp (LinearMap.snd R M M₃) +
f.comp
(LinearMap.fst R M
M₃)) with
invFun := fun p : M₂ × M₄ => (e₁.symm p.1, e₂.symm (p.2 - f (e₁.symm p.1)))
left_inv := fun p => by simp
right_inv := fun p => by simp }
