Commit 2025-08-13 13:22 ed52228d

View on Github →

chore: defer imports of orderOf (#28318) See #mathlib4 > Warning that AlgebraicTopology can't import SetTheory

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean

Modified Mathlib/Analysis/Normed/Module/Ray.lean

Created Mathlib/Analysis/Normed/Ring/Finite.lean

added theorem AddChar.norm_apply

Modified Mathlib/Analysis/Normed/Ring/Lemmas.lean

deleted theorem AddChar.norm_apply

Modified Mathlib/Analysis/NormedSpace/Connected.lean

Modified Mathlib/Analysis/RCLike/Basic.lean