Commit 2025-07-07 17:19 55cdebc8

View on Github →

chore: golf using exact (#26654)

Estimated changes

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean

Modified Mathlib/Analysis/Normed/Group/Quotient.lean

modified theorem quotient_norm_add_le

Modified Mathlib/Analysis/SpecialFunctions/Log/Base.lean

Modified Mathlib/Data/TypeVec.lean

modified theorem TypeVec.prod_map_id

Modified Mathlib/FieldTheory/Separable.lean

Modified Mathlib/Geometry/Euclidean/SignedDist.lean

Modified Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean

Modified Mathlib/RingTheory/EssentialFiniteness.lean