English
To prove a property for arbitrary finite products of modules, it suffices to prove stability under isomorphism, validity for the zero module, and stability under taking products of components.
Русский
Чтобы доказать свойство для произвольных конечных произведений модулей, достаточно доказать инвариантность под изоморфизмами, верность для нулевого модуля и устойчивость к произведению компонент.
LaTeX
$$$$ \\text{pi\_induction: }(\\forall N)[AddCommMonoid N] [Module R N] \\rightarrow (\\forall N')[AddCommMonoid N'] [Module R N'] \\rightarrow \\cdots $$$$
Lean4
/-- `Fin.consEquiv` as a continuous linear equivalence. -/
@[simps]
def consLinearEquiv {n : ℕ} (M : Fin n.succ → Type*) [Semiring R] [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)] :
(M 0 × Π i, M (Fin.succ i)) ≃ₗ[R] (Π i, M i)
where
__ := Fin.consEquiv M
map_add' x y := funext <| Fin.cases rfl (by simp)
map_smul' c x := funext <| Fin.cases rfl (by simp)
