Theorem norm_zsmul

Modification history

2024-08-12 18:29

Mathlib/Analysis/Normed/Module/Basic.lean

chore: move to v4.11.0-rc2 (new `variable` command) (#15726)

Modified norm_zsmul View on Github →

2024-02-24 23:45

Mathlib/Analysis/NormedSpace/Basic.lean

chore(NormedSpace/Basic): rename type variables (#10863) …

Modified norm_zsmul View on Github →

2023-04-12 19:26

Mathlib/Analysis/NormedSpace/Basic.lean

feat: port Analysis.NormedSpace.Basic (#3280)

Added norm_zsmul View on Github →