Documentation

MeanFourier.Mathlib.Topology.Algebra.Module.Equiv

source
@[simp]
theorem ContinuousLinearEquiv.toLinearEquiv_one {R : Type u_1} {M : Type u_2} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] :
↑1 = 1
source
@[simp]
theorem ContinuousLinearEquiv.toLinearEquiv_mul {R : Type u_1} {M : Type u_2} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] (e e' : M ≃L[R] M) :
↑(e * e') = ↑e * ↑e'