Linear map extensionality

3/4 ~20 minlean

Prove two linear maps equal from pointwise equality.

7 lines · Lean 4

import Mathlib

example {R M N : Type} [Semiring R]
    [AddCommMonoid M] [Module R M]
    [AddCommMonoid N] [Module R N]
    (f g : M →ₗ[R] N) (h : ∀ x, f x = g x) : f = g := by
  sorry

Objectifs

Prove two linear maps equal from pointwise equality.

Indices

Voir la solution

import Mathlib

example {R M N : Type} [Semiring R]
    [AddCommMonoid M] [Module R M]
    [AddCommMonoid N] [Module R N]
    (f g : M →ₗ[R] N) (h : ∀ x, f x = g x) : f = g := by
  ext x
  exact h x