Commit 2024-02-13 12:46 678a9b1b

View on Github →

chore: tidy various files (#10453)

Estimated changes

Modified Mathlib/Algebra/Category/GroupCat/Basic.lean

Modified Mathlib/Algebra/Category/MonCat/Basic.lean

Modified Mathlib/Algebra/Group/Defs.lean

Modified Mathlib/Algebra/Ring/Units.lean

Modified Mathlib/CategoryTheory/ConcreteCategory/Bundled.lean

Modified Mathlib/Data/Fintype/Basic.lean

added theorem Fintype.univ_ofIsEmpty

deleted theorem Fintype.univ_of_isEmpty

Modified Mathlib/Data/Fintype/Card.lean

added theorem Fintype.card_ofIsEmpty

deleted theorem Fintype.card_of_isEmpty

Modified Mathlib/MeasureTheory/Decomposition/Lebesgue.lean

Modified Mathlib/RingTheory/WittVector/Defs.lean

modified theorem WittVector.add_coeff

modified theorem WittVector.mul_coeff

modified theorem WittVector.pow_coeff

modified theorem WittVector.sub_coeff

Modified Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean