mulAction' — Mathlib

English

Induction principle on M/P: to prove a statement for every element of M/P it suffices to prove it for images of all x ∈ M via the quotient map.

Русский

Индукционный принцип на M/P: чтобы доказать утверждение для каждого элемента M/P, достаточно доказать его для образов всех x ∈ M через квазиобразующую карту.

LaTeX

$$$\forall C : (M ⧸ p) \to \mathrm{Prop},\ x \in M ⧸ p,\ (\forall z \in M,\ C(\mathrm{Quotient.mk}\ z)) \Rightarrow C(x)$$$

Lean4

instance mulAction' [Monoid S] [SMul S R] [MulAction S M] [IsScalarTower S R M] (P : Submodule R M) :
    MulAction S (M ⧸ P) :=
  fast_instance%Function.Surjective.mulAction mk Quot.mk_surjective <| Submodule.Quotient.mk_smul P

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