pi_toSubmodule — Mathlib

English

The underlying submodule of the pi construction is the pi of the underlying submodules of the t_i.

Русский

У подструктуры, соответствующей конструктору π, есть ядро: подмодуль π( s, t ) равен произведению подмодулей (t_i).

LaTeX

$$$toSubmodule(\pi(s,t)) = \pi(s, i\mapsto toSubmodule(t_i))$$$

Lean4

@[simp]
theorem pi_toSubmodule : toSubmodule (pi s t) = .pi s fun i ↦ (t i).toSubmodule :=
  rfl

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