Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-18 11:01 0e995a37

View on Github →

refactor(*): kill a few uses of finish (#10860)

Estimated changes

Modified src/algebra/big_operators/ring.lean

Modified src/analysis/convex/basic.lean

modified theorem convex_empty

Modified src/analysis/normed_space/lattice_ordered_group.lean

Modified src/data/set/constructions.lean

Modified src/data/set/lattice.lean