Commit 2023-04-22 02:22 3a1848ee

View on Github →

chore: tidy various files (#3584)

Estimated changes

Modified Mathlib/Algebra/Algebra/Equiv.lean

modified def AlgEquiv.autCongr

added theorem AlgEquiv.refl_toAlgHom

deleted theorem AlgEquiv.refl_to_algHom

added theorem AlgEquiv.symm_toRingEquiv

deleted theorem AlgEquiv.symm_to_ringEquiv

added theorem AlgEquiv.toAlgHom_toLinearMap

added theorem AlgEquiv.toRingEquiv_symm

deleted theorem AlgEquiv.to_algHom_toLinearMap

deleted theorem AlgEquiv.to_ringEquiv_symm

Modified Mathlib/CategoryTheory/Filtered.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean

modified theorem CategoryTheory.Limits.IsInitial.hasInitial

Modified Mathlib/Combinatorics/SimpleGraph/Density.lean

Modified Mathlib/Data/Bitvec/Basic.lean

Modified Mathlib/Data/Real/ConjugateExponents.lean

deleted theorem Real.IsConjugateExponent.inv_add_inv_conj_nNReal

added theorem Real.IsConjugateExponent.inv_add_inv_conj_nnreal

deleted theorem Real.IsConjugateExponent.one_lt_nNReal

added theorem Real.IsConjugateExponent.one_lt_nnreal

Modified Mathlib/Dynamics/OmegaLimit.lean

modified theorem Flow.omegaLimit_image_subset

added theorem mapsTo_omegaLimit'

deleted theorem mapsTo_omega_limit'

deleted theorem omegaLimit_eq_bInter_inter

added theorem omegaLimit_eq_binterᵢ_inter