Commit 2024-01-19 22:02 0a33acc5

View on Github →

chore: tidy various files (#9851)

Estimated changes

Modified Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

Modified Mathlib/Algebra/Group/PNatPowAssoc.lean

Modified Mathlib/Algebra/Order/Module/Defs.lean

Modified Mathlib/Data/PNat/Factors.lean

modified theorem PrimeMultiset.prod_smul

Modified Mathlib/Data/Polynomial/RingDivision.lean

Modified Mathlib/Data/Set/Finite.lean

modified theorem Set.empty_card'

Modified Mathlib/Data/Set/Pointwise/Basic.lean

Modified Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean

Modified Mathlib/FieldTheory/Separable.lean

Modified Mathlib/Geometry/Manifold/InteriorBoundary.lean

modified theorem ModelWithCorners.interior_eq_univ

Modified Mathlib/GroupTheory/Subsemigroup/Center.lean

Modified Mathlib/LinearAlgebra/Basis.lean

Modified Mathlib/LinearAlgebra/Dimension/Finite.lean

Modified Mathlib/LinearAlgebra/Dual.lean

Modified Mathlib/LinearAlgebra/Matrix/Hermitian.lean

modified theorem Matrix.isHermitian_diagonal_iff

Modified Mathlib/NumberTheory/ArithmeticFunction.lean

Modified Mathlib/Probability/Process/Stopping.lean

Modified Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean

Modified Mathlib/RingTheory/Finiteness.lean

Modified Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean

Modified Mathlib/Tactic/ModCases.lean