Commit 2025-04-28 03:19 70fb092b

View on Github →

chore(Asymptotics/TVS): add a whitespace to notation (#24425) I think that we should put whitespaces after punctuation.

Estimated changes

Modified Mathlib/Analysis/Asymptotics/TVS.lean

modified theorem Asymptotics.IsLittleOTVS.bot

modified theorem Asymptotics.IsLittleOTVS.congr'

modified theorem Asymptotics.IsLittleOTVS.congr

modified theorem Asymptotics.IsLittleOTVS.congr_left

modified theorem Asymptotics.IsLittleOTVS.congr_right

modified theorem Asymptotics.IsLittleOTVS.mono

modified theorem Asymptotics.IsLittleOTVS.tendsto_inv_smul

modified theorem Asymptotics.IsLittleOTVS.trans

modified theorem Asymptotics.IsLittleOTVS.zero

modified theorem Asymptotics.isLittleOTVS_one

Modified Mathlib/Analysis/Calculus/FDeriv/Basic.lean