Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-15 23:05 c1a5ae94

View on Github →

chore(order/directed): use implicit args in iffs (#3411)

Estimated changes

Modified src/analysis/convex/cone.lean

Modified src/group_theory/subgroup.lean

Modified src/group_theory/submonoid/membership.lean

Modified src/linear_algebra/basic.lean

Modified src/linear_algebra/basis.lean

Modified src/linear_algebra/linear_pmap.lean

Modified src/order/complete_lattice.lean

added theorem Sup_eq_supr'

Modified src/order/directed.lean

modified theorem directed_comp

Modified src/ring_theory/subsemiring.lean

Modified src/topology/algebra/infinite_sum.lean