Commit 2024-10-31 05:46 d9273054

View on Github →

chore: deal with porting notes about 'protected' (#18368)

Estimated changes

Modified Mathlib/Algebra/Algebra/Equiv.lean

Modified Mathlib/Algebra/GroupWithZero/Divisibility.lean

Modified Mathlib/Algebra/ModEq.lean

Modified Mathlib/Algebra/Ring/Int.lean

Modified Mathlib/Analysis/Normed/Field/Lemmas.lean

Modified Mathlib/Analysis/Normed/Group/Basic.lean

Modified Mathlib/Analysis/Normed/Group/Bounded.lean

Modified Mathlib/Analysis/Normed/Group/Uniform.lean

Modified Mathlib/Analysis/Oscillation.lean

Modified Mathlib/CategoryTheory/Category/Pointed.lean

Modified Mathlib/Data/ENNReal/Operations.lean

deleted theorem ENNReal.add_lt_add

deleted theorem ENNReal.mul_sub

deleted theorem ENNReal.sub_mul

Modified Mathlib/Data/List/Nodup.lean

Modified Mathlib/Data/List/Pairwise.lean

Modified Mathlib/Data/List/Perm/Subperm.lean

Modified Mathlib/Data/List/Sublists.lean

Modified Mathlib/Data/Nat/Prime/Basic.lean

Modified Mathlib/Data/Real/EReal.lean

deleted theorem EReal.div_eq_inv_mul

Modified Mathlib/Data/Set/Finite.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean

Modified Mathlib/LinearAlgebra/ExteriorAlgebra/Grading.lean

Modified Mathlib/LinearAlgebra/Ray.lean

Modified Mathlib/ModelTheory/Semantics.lean

Modified Mathlib/NumberTheory/FunctionField.lean

Modified Mathlib/Order/Directed.lean

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

Modified Mathlib/Order/Irreducible.lean

Modified Mathlib/Order/Partition/Finpartition.lean

Modified Mathlib/Topology/Algebra/Group/Basic.lean

Modified Mathlib/Topology/Instances/ENNReal.lean

Modified Mathlib/Topology/MetricSpace/Dilation.lean

deleted theorem Dilation.coe_id