Theorem InnerProductSpace.Core.inner_smul_ofReal_left

Modification history

2024-08-15 08:47

Mathlib/Analysis/InnerProductSpace/Basic.lean

chore: tidy various files (#15807)

Modified InnerProductSpace.Core.inner_smul_ofReal_left View on Github →

2024-08-07 01:32

Mathlib/Analysis/InnerProductSpace/Basic.lean

feat(Analysis/InnerProductSpace/Basic): add PreInnerProductSpace (#14024) …

Added InnerProductSpace.Core.inner_smul_ofReal_left View on Github →