Commit 2025-07-04 10:05 c14c4461

View on Github →

chore: whitespace before : (#26727) Found by #26718.

Estimated changes

Modified Mathlib/Algebra/Algebra/Subalgebra/Directed.lean

Modified Mathlib/Algebra/BrauerGroup/Defs.lean

deleted def Brauer.CSA_Setoid:

added def Brauer.CSA_Setoid

Modified Mathlib/Algebra/DirectSum/Idempotents.lean

modified theorem DirectSum.completeOrthogonalIdempotents_idempotent

Modified Mathlib/Algebra/Group/Subgroup/Map.lean

modified theorem Subgroup.map_toSubmonoid

Modified Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean

Modified Mathlib/Algebra/Lie/Nilpotent.lean

deleted theorem LieSubmodule.lowerCentralSeries_eq_bot_iff_lcs_eq_bot:

added theorem LieSubmodule.lowerCentralSeries_eq_bot_iff_lcs_eq_bot

Modified Mathlib/Algebra/Module/Submodule/Ker.lean

Modified Mathlib/Algebra/Module/ZLattice/Covolume.lean

Modified Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean

Modified Mathlib/Algebra/Ring/Semireal/Defs.lean

modified theorem IsSemireal.not_isSumSq_neg_one

Modified Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean

Modified Mathlib/AlgebraicGeometry/Modules/Tilde.lean

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

modified theorem Filter.EventuallyEq.congr_contDiffWithinAt_of_mem

Modified Mathlib/Analysis/Calculus/LogDeriv.lean

modified theorem logDeriv_const_mul

modified theorem logDeriv_mul_const

Modified Mathlib/Analysis/Complex/Positivity.lean

Modified Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean

Modified Mathlib/Analysis/Normed/Lp/WithLp.lean

modified theorem WithLp.equiv_symm_neg

Modified Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean

Modified Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean

modified theorem integrableOn_Ioi_deriv_norm_ofReal_cpow

Modified Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean

Modified Mathlib/CategoryTheory/Join/Basic.lean

deleted def CategoryTheory.Join.inclLeftFullyFaithful:

added def CategoryTheory.Join.inclLeftFullyFaithful

deleted def CategoryTheory.Join.inclRightFullyFaithful:

added def CategoryTheory.Join.inclRightFullyFaithful

Modified Mathlib/CategoryTheory/Monoidal/End.lean

modified theorem CategoryTheory.left_unitality_app

modified theorem CategoryTheory.obj_ε_app

modified theorem CategoryTheory.obj_μ_zero_app

modified theorem CategoryTheory.δ_naturality

modified theorem CategoryTheory.δ_naturalityᵣ

modified theorem CategoryTheory.η_naturality

modified theorem CategoryTheory.μ_naturalityₗ

Modified Mathlib/CategoryTheory/MorphismProperty/Descent.lean

Modified Mathlib/CategoryTheory/Sites/GlobalSections.lean

Modified Mathlib/Data/Matrix/RowCol.lean

Modified Mathlib/Data/Quot.lean

Modified Mathlib/Data/Vector/MapLemmas.lean

modified theorem List.Vector.map_pmap

Modified Mathlib/GroupTheory/FixedPointFree.lean

modified def MonoidHom.FixedPointFree.commGroupOfInvolutive

Modified Mathlib/GroupTheory/GroupAction/Basic.lean

Modified Mathlib/GroupTheory/OrderOfElement.lean

modified theorem Commute.orderOf_dvd_lcm_mul

modified theorem Commute.orderOf_mul_dvd_mul_orderOf

Modified Mathlib/GroupTheory/Perm/DomMulAct.lean

deleted theorem DomMulAct.stabilizer_card':

added theorem DomMulAct.stabilizer_card'

Modified Mathlib/LinearAlgebra/LinearIndependent/Defs.lean

deleted theorem linearIndepOn_iff_disjoint:

added theorem linearIndepOn_iff_disjoint

Modified Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean

modified theorem linearIndepOn_pair_iff

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean

Modified Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

modified theorem MeasureTheory.eLpNorm_const_smul

Modified Mathlib/MeasureTheory/Group/Convolution.lean

Modified Mathlib/ModelTheory/ElementarySubstructures.lean

modified theorem FirstOrder.Language.ElementarySubstructure.subtype_injective

Modified Mathlib/ModelTheory/Substructures.lean

modified theorem FirstOrder.Language.Substructure.subtype_injective

Modified Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean

modified theorem SL_reduction_mod_hom_val

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

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

modified theorem NumberField.mixedEmbedding.fundamentalCone.hasFDerivAt_expMap

Modified Mathlib/NumberTheory/RamificationInertia/Galois.lean

modified theorem Ideal.coe_smul_primesOver_eq_map_galRestrict

Modified Mathlib/Order/Interval/Finset/Defs.lean

modified theorem Finset.map_subtype_embedding_Icc

modified theorem Finset.map_subtype_embedding_Ico

modified theorem Finset.map_subtype_embedding_Ioc

modified theorem Finset.map_subtype_embedding_Ioo

Modified Mathlib/Order/Interval/Set/Pi.lean

modified theorem Set.pi_univ_Ico_subset

modified theorem Set.pi_univ_Iio_subset

modified theorem Set.pi_univ_Ioc_subset

modified theorem Set.pi_univ_Ioi_subset

modified theorem Set.pi_univ_Ioo_subset

Modified Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean

deleted theorem groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom:

added theorem groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom

Modified Mathlib/RingTheory/Polynomial/GaussNorm.lean

modified theorem PowerSeries.gaussNorm_monomial

Modified Mathlib/RingTheory/PowerSeries/Evaluation.lean

Modified Mathlib/RingTheory/Valuation/Minpoly.lean

modified theorem Valuation.pow_coeff_zero_ne_zero_of_unit

Modified Mathlib/SetTheory/Ordinal/Family.lean

modified theorem Ordinal.iSup_sum

Modified Mathlib/Tactic/Widget/Conv.lean

Modified Mathlib/Topology/Algebra/Monoid.lean

Modified Mathlib/Topology/Algebra/Valued/NormedValued.lean

deleted def Valued.toNontriviallyNormedField:

added def Valued.toNontriviallyNormedField

Modified Mathlib/Topology/Category/TopCat/Limits/Basic.lean

modified theorem TopCat.colimit_topology

modified theorem TopCat.limit_topology

Modified Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean

Modified Mathlib/Topology/ContinuousOn.lean

Modified Mathlib/Topology/LocallyFinsupp.lean

Modified Mathlib/Topology/Order/IsLUB.lean