@[simp]

theorem LinearEquiv.toLinearMap_one {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] : ↑1 = 1