English
The prodEquivOfIsCompl p q h maps a pair (a,b) to the sum a+b in E; i.e., it identifies the product with E by adding the two coordinates.
Русский
prodEquivOfIsCompl p q h отображает пару (a,b) в сумму a+b в E; то есть идентифицирует произведение с E суммированием координат.
LaTeX
$$$prodEquivOfIsCompl p q h (a,b) = a+b$$$
Lean4
/-- If `q` is a complement of `p`, then `p × q` is isomorphic to `E`. -/
def prodEquivOfIsCompl (h : IsCompl p q) : (p × q) ≃ₗ[R] E :=
by
apply LinearEquiv.ofBijective (p.subtype.coprod q.subtype)
constructor
· rw [← ker_eq_bot, ker_coprod_of_disjoint_range, ker_subtype, ker_subtype, prod_bot]
rw [range_subtype, range_subtype]
exact h.1
· rw [← range_eq_top, ← sup_eq_range, h.sup_eq_top]
