prodCongr_toContinuousAffineMap — Mathlib

English

The underlying continuous affine map of the product is the product of the underlying continuous maps: (e₁.prodCongr e₂).toContinuousAffineMap = e₁.toContinuousAffineMap.prodMap e₂.toContinuousAffineMap.

Русский

Базовая непрерывная аффинная карта у произведения равна произведению базовых непрерывных карт: (e₁.prodCongr e₂).toContinuousAffineMap = e₁.toContinuousAffineMap.prodMap e₂.toContinuousAffineMap.

LaTeX

$$$ (e_1.prodCongr e_2).toContinuousAffineMap = e_1.toContinuousAffineMap.prodMap e_2.toContinuousAffineMap. $$$

Lean4

@[simp]
theorem prodCongr_toContinuousAffineMap :
    (e₁.prodCongr e₂).toContinuousAffineMap = e₁.toContinuousAffineMap.prodMap e₂.toContinuousAffineMap :=
  rfl

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