mul — Mathlib

English

For x, y ∈ PreTilt(O,p) and any m, p^m divides ((x·y).untiltAux m) − (x.untiltAux m)(y.untiltAux m).

Русский

Для x, y ∈ PreTilt(O,p) и любого m, p^m делит ((x·y).untiltAux m) − (x.untiltAux m)(y.untiltAux m).

LaTeX

$$$(p : O)^m \mid ((x \cdot y).untiltAux m) - (x.untiltAux m)(y.untiltAux m)$$$

Lean4

/-- The multiplication in tensor product of rings is induced by `(xᵢ) * (yᵢ) = (xᵢ * yᵢ)`
-/
def mul : (⨂[R] i, A i) →ₗ[R] (⨂[R] i, A i) →ₗ[R] (⨂[R] i, A i) :=
  PiTensorProduct.piTensorHomMap₂ <| tprod R fun _ ↦ LinearMap.mul _ _

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