Commit 2025-03-12 15:37 4f974b07

View on Github →

chore(whitespace): more whitespace changes (#22850) Found by #22760.

Estimated changes

Modified Mathlib/Algebra/Group/Invertible/Defs.lean

Modified Mathlib/Algebra/Homology/HomologicalComplex.lean

Modified Mathlib/CategoryTheory/Limits/VanKampen.lean

modified theorem CategoryTheory.NatTrans.Equifibered.whiskerLeft

Modified Mathlib/CategoryTheory/Sites/CoverPreserving.lean

Modified Mathlib/MeasureTheory/Integral/Gamma.lean

modified theorem Complex.integral_rpow_mul_exp_neg_mul_rpow

modified theorem Complex.integral_rpow_mul_exp_neg_rpow

modified theorem integral_rpow_mul_exp_neg_mul_rpow

modified theorem integral_rpow_mul_exp_neg_rpow

Modified Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean

Modified Mathlib/ModelTheory/Encoding.lean

modified theorem FirstOrder.Language.BoundedFormula.card_le

modified theorem FirstOrder.Language.BoundedFormula.listDecode_encode_list

modified def FirstOrder.Language.BoundedFormula.sigmaAll

modified def FirstOrder.Language.BoundedFormula.sigmaImp

modified theorem FirstOrder.Language.Term.card_le

modified theorem FirstOrder.Language.Term.card_sigma

modified def FirstOrder.Language.Term.listDecode

modified def FirstOrder.Language.Term.listEncode

Modified Mathlib/ModelTheory/FinitelyGenerated.lean

modified theorem FirstOrder.Language.Structure.cg_iff_countable

modified theorem FirstOrder.Language.Substructure.cg_iff_countable

Modified Mathlib/ModelTheory/PartialEquiv.lean

modified theorem FirstOrder.Language.Embedding.toPartialEquiv_toEmbedding

Modified Mathlib/ModelTheory/Semantics.lean

Modified Mathlib/ModelTheory/Substructures.lean

Modified Mathlib/NumberTheory/AbelSummation.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean

modified theorem NumberField.mixedEmbedding.normAtPlace_neg

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/PolarCoord.lean

modified theorem NumberField.mixedEmbedding.integral_comp_polarCoordReal_symm

Modified Mathlib/Probability/Independence/Integrable.lean

Modified Mathlib/Tactic/CategoryTheory/Bicategory/Datatypes.lean

Modified Mathlib/Tactic/CategoryTheory/Bicategory/Normalize.lean

Modified Mathlib/Topology/Sheaves/Stalks.lean

modified theorem TopCat.Presheaf.app_isIso_of_stalkFunctor_map_iso