An example of formalization

Stream: general

[Andrej Bauer]

I am going to talk about formalized math on Thursday at the European congrees of mathematics and I'd like to show some examples of Lean. I can produce my own, but I am likely going to miss some idioms as I have not used Lean much (yet). Is there a nice soul that could produce a Lean snippet which expresses the following:

If f is linear then f(2 · x + y) = 2 · f(x) + f(y).

Feel free to interpret "linear" so that it fits existing things in the library. (I had vector spaces in mind.) The point of the example should be to show what needs to be done when one takes a statement and formalizes it in a proof assistant. I am trying to showcase existing technology (type classes, notations, implicit arguments, et.c) Many thanks!

For reference, here is how I intend to elaborate the statement in "human math":

If K is a field, U and V are vector spaces over K,
and f : |U| → |V| is linear then, for all x, y ∈ |U|,
f(2_K ·_U x +_U y) = 2_K ·_V f(x) +_V f(y).

[Adam Topaz]

import linear_algebra

variables (K : Type*) [field K] (V W : Type*) [add_comm_group V] [add_comm_group W]
  [module K V] [module K W] (f : V →ₗ[K] W)

example {v1 v2 : V} : f (2 • v1 + v2) = 2 • f v1 + f v2 := by simp

[Adam Topaz]

V →ₗ[K] W is notation for the type of K-linear maps from V to W

[Anne Baanen]

Beware that 2 is interpreted as a natural number, the proof is more specifically:

by rw [linear_map.map_add f (2 • x) y, linear_map.map_smul_of_tower f (2 : ℕ) x]

[Adam Topaz]

This works if you want to use the 2 : K:

import linear_algebra

variables (K : Type*) [field K] (V W : Type*) [add_comm_group V] [add_comm_group W]
  [module K V] [module K W] (f : V →ₗ[K] W)

example {v1 v2 : V} : f ((2 : K) • v1 + v2) = (2 : K) • f v1 + f v2 := by simp