Commit 2024-02-24 23:45 c8eaa189

View on Github →

chore(NormedSpace/Basic): rename type variables (#10863) Also use letI for theorems about non-canonical instances.

Estimated changes

Modified Mathlib/Analysis/NormedSpace/Basic.lean

modified theorem Filter.IsBoundedUnder.smul_tendsto_zero

modified theorem Filter.Tendsto.zero_smul_isBoundedUnder_le

modified def NormedAlgebra.induced

modified def NormedSpace.induced

modified theorem eventually_nhds_norm_smul_sub_lt

modified theorem norm_zsmul