eqLocus — Mathlib

English

Continuation of the construction showing closure under scalar multiplication and addition on the subtype.

Русский

Продолжение построения, показывающее замкнутость подтипа по умножению на скаляры и сложению.

LaTeX

$$Module'\text{proof}_2$$

Lean4

/-- A linear map version of `AddMonoidHom.eqLocusM` -/
def eqLocus (f g : F) : Submodule R M :=
  { (f : M →+ M₂).eqLocusM g with
    carrier := {x | f x = g x}
    smul_mem' := fun {r} {x} (hx : _ = _) =>
      show _ = _ by
        -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 changed `map_smulₛₗ` into `map_smulₛₗ _`
        simpa only [map_smulₛₗ _] using congr_arg (τ₁₂ r • ·) hx }

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