Commit 2023-06-19 05:31 697ac1d3

View on Github →

chore: tidy various files (#5233)

Estimated changes

Modified Archive/Imo/Imo2011Q5.lean

Modified Archive/Imo/Imo2019Q4.lean

Modified Mathlib/Algebra/Group/Defs.lean

Modified Mathlib/Algebra/Lie/OfAssociative.lean

added theorem AlgHom.coe_toLieHom

deleted theorem AlgHom.coe_to_lieHom

added theorem AlgHom.toLieHom_comp

added theorem AlgHom.toLieHom_id

added theorem AlgHom.toLieHom_injective

deleted theorem AlgHom.to_lieHom_comp

deleted theorem AlgHom.to_lieHom_id

deleted theorem AlgHom.to_lieHom_injective

Modified Mathlib/Algebra/Lie/UniversalEnveloping.lean

Modified Mathlib/Algebra/NeZero.lean

Modified Mathlib/Algebra/Order/Monoid/NatCast.lean

Modified Mathlib/Analysis/Analytic/IsolatedZeros.lean

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.lean

Modified Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean

Modified Mathlib/Data/Vector3.lean

Modified Mathlib/FieldTheory/Fixed.lean

Modified Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean

Modified Mathlib/LinearAlgebra/Matrix/LDL.lean

Modified Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean

Modified Mathlib/MeasureTheory/Group/FundamentalDomain.lean

deleted theorem MeasureTheory.IsFundamentalDomain.pairwise_aEDisjoint_of_ac

added theorem MeasureTheory.IsFundamentalDomain.pairwise_aedisjoint_of_ac

Modified Mathlib/Order/Category/BoolAlgCat.lean

Modified Mathlib/RingTheory/LocalProperties.lean

Modified Mathlib/Topology/Algebra/ValuedField.lean

Modified Mathlib/Topology/Category/UniformSpace.lean