Commit 2025-02-17 04:08 6b0da400

View on Github →

chore(LocallyConvex/Basic): generalize TC assumptions (#21942) ... from NormedField to NormedDivisionRing in some lemmas.

Estimated changes

Modified Mathlib/Analysis/LocallyConvex/Basic.lean

modified theorem Balanced.absorbs_self

modified theorem Balanced.smul_congr

modified theorem Balanced.smul_eq

modified theorem Balanced.smul_mem_mono

modified theorem Balanced.smul_mono

modified theorem Balanced.subset_smul