Commit 2024-08-18 04:33 bbc4793a

View on Github →

chore: remove bare open Classical, part 6 (#15837)

Estimated changes

Modified Mathlib/LinearAlgebra/Trace.lean

modified theorem LinearMap.trace_mul_comm

Modified Mathlib/Order/Filter/Ultrafilter.lean

Modified Mathlib/Order/SuccPred/Basic.lean

Modified Mathlib/Order/Zorn.lean

Modified Mathlib/SetTheory/Cardinal/Finsupp.lean

modified theorem Cardinal.mk_multiset_of_countable

modified theorem Cardinal.mk_multiset_of_nonempty

Modified Mathlib/Topology/Algebra/InfiniteSum/Order.lean

modified theorem isLUB_hasProd'

Modified Mathlib/Topology/Algebra/InfiniteSum/Ring.lean

modified theorem Commute.tsum_right

modified theorem tsum_mul_left

modified theorem tsum_mul_right

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

Modified Mathlib/Topology/Algebra/Module/LinearPMap.lean

Modified Mathlib/Topology/Algebra/Monoid.lean

Modified Mathlib/Topology/Algebra/Order/LiminfLimsup.lean

Modified Mathlib/Topology/Algebra/Valued/ValuationTopology.lean