Commit 2024-11-23 22:52 b5155f3e

View on Github →

chore: more simpNF cleanup (#19395)

Estimated changes

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean

deleted theorem MultilinearMap.curryFinFinset_apply_const_aux

deleted theorem MultilinearMap.curryFinFinset_symm_apply_piecewise_const_aux

Modified Mathlib/NumberTheory/Modular.lean

Modified Mathlib/NumberTheory/ModularForms/SlashActions.lean

added theorem ModularForm.is_invariant_one'

Modified Mathlib/NumberTheory/Padics/PadicIntegers.lean

modified theorem PadicInt.intCast_eq

modified theorem PadicInt.mk_coe

modified theorem PadicInt.norm_p_pow

added theorem PadicInt.not_isUnit_iff

Modified Mathlib/NumberTheory/Padics/RingHoms.lean

Modified Mathlib/Order/Closure.lean

Modified Mathlib/Order/Compare.lean

Modified Mathlib/Order/Filter/Germ/Basic.lean

Modified Mathlib/Order/Filter/Pointwise.lean

modified theorem Filter.pure_div_pure

modified theorem Filter.pure_mul_pure

modified theorem Filter.pure_smul_pure

modified theorem Filter.pure_vsub_pure

Modified Mathlib/Order/Heyting/Basic.lean

Modified Mathlib/Order/Interval/Basic.lean

Modified Mathlib/Order/LiminfLimsup.lean

Modified Mathlib/Order/SupIndep.lean

Modified Mathlib/RingTheory/DedekindDomain/SInteger.lean

Modified Mathlib/RingTheory/Ideal/Operations.lean

Modified Mathlib/RingTheory/Valuation/Basic.lean

Modified Mathlib/RingTheory/Valuation/ValuationSubring.lean