colimitSMulWithZero — Mathlib

English

The unit axiom follows from the surjectivity of mk and the construction of smul.

Русский

Аксиома единицы следует из сюръективности mk и конструктивности умножения.

LaTeX

$$$$ (1)\\cdot x = x $$$$

Lean4

instance colimitSMulWithZero : SMulWithZero R (M F) :=
  {
    colimitMulAction
      F with
    smul_zero := fun r => by rw [colimit_zero_eq _ (IsFiltered.nonempty.some : J), colimit_smul_mk_eq, smul_zero]
    zero_smul := fun x => by
      obtain ⟨j, x, rfl⟩ := M.mk_surjective F x
      simp [← colimit_zero_eq] }

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