English
Let b be a basis of M indexed by ι and b' a basis of M' indexed by ι'. Then there exists a natural basis of M × M' indexed by ι ⊕ ι', obtained from b and b' by taking their product; this basis is denoted by b.prod b'.
Русский
Пусть b — базис M, индексированный ι, и b' — базис M', индексированный ι'. Тогда существует естественный базис M × M', индексируемый суммой ι ⊕ ι', получаемый как произведение базисов b и b' и обозначаемый b.prod b'.
LaTeX
$$$ (b \mathrm{prod} b') : \mathrm{Basis}(\iota \oplus \iota')\; R\; (M \times M') $$$
Lean4
/-- `Basis.prod` maps an `ι`-indexed basis for `M` and an `ι'`-indexed basis for `M'`
to an `ι ⊕ ι'`-index basis for `M × M'`.
For the specific case of `R × R`, see also `Basis.finTwoProd`. -/
protected def prod : Basis (ι ⊕ ι') R (M × M') :=
ofRepr ((b.repr.prodCongr b'.repr).trans (Finsupp.sumFinsuppLEquivProdFinsupp R).symm)
