Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(algebra/linear_ordered_comm_group_with_zero): Add linear_ordered_comm_monoid_with_zero and an instance for nat #5645

Closed
wants to merge 11 commits into from
Closed

[Merged by Bors] - feat(algebra/linear_ordered_comm_group_with_zero): Add linear_ordered_comm_monoid_with_zero and an instance for nat #5645

wants to merge 11 commits into from

Conversation

eric-wieser
Copy link
Member

@eric-wieser eric-wieser commented Jan 6, 2021 •
edited
Loading

This generalizes a lot of statements about linear_ordered_comm_group_with_zero to linear_ordered_comm_monoid_with_zero.

Zulip.

This extends on the suggestion there, and add a new typeclass to sit between ordered_comm_monoid and linear_ordered_comm_group_with_zero, at the position where an instance for nat can exist.

@eric-wieser eric-wieser added the awaiting-review The author would like community review of the PR label Jan 6, 2021
jcommelin
jcommelin reviewed Jan 7, 2021
View reviewed changes
src/algebra/ordered_monoid.lean Outdated
extends linear_order α, comm_monoid_with_zero α, ordered_comm_monoid α :=
(zero_le_one : (0:α) ≤ 1)
(lt_of_mul_lt_mul_left := λ x y z, by {
-- type-class inference uses a meaningless `linear_order` without this!
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But how can it even find that meaningless instance? I'm a bit confused...

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Try it and see?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've clarified the comment a bit and golfed the proof, although the trick is still here.

jcommelin
jcommelin approved these changes Jan 8, 2021
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Jan 8, 2021
bors bot pushed a commit that referenced this pull request Jan 8, 2021
@eric-wieser
feat(algebra/linear_ordered_comm_group_with_zero): Add linear_ordered…
d935760 
…_comm_monoid_with_zero and an instance for nat (#5645)

This generalizes a lot of statements about `linear_ordered_comm_group_with_zero` to `linear_ordered_comm_monoid_with_zero`.
@bors
Copy link

bors bot commented Jan 8, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(algebra/linear_ordered_comm_group_with_zero): Add linear_ordered_comm_monoid_with_zero and an instance for nat [Merged by Bors] - feat(algebra/linear_ordered_comm_group_with_zero): Add linear_ordered_comm_monoid_with_zero and an instance for nat Jan 8, 2021
@bors bors bot closed this Jan 8, 2021
@bors bors bot deleted the eric-wieser/kbuzzard-nat-instance branch January 8, 2021 20:24
Julian added a commit that referenced this pull request Jan 12, 2021
@Julian
Merge remote-tracking branch 'origin/master' into freek-45
2be7703 
* origin/master: (751 commits)
  chore(topology/algebra/infinite_sum): speedup has_sum_sum (#5710)
  feat(submonoid/basic): subsingleton and nontrivial instances for {add_,}submonoid (#5690)
  docs(undergrad.yaml): analysis updates (#5675)
  feat(linear_algebra/multilinear_map): Add `range` and `map` (#5658)
  feat(measure_theory): each set has a measurable superset of the same measure (#5688)
  feat(data/set/intervals): add 2 Icc ssubset lemmas (#5617)
  chore(category_theory/limits): move constructions folder (#5681)
  fix(linear_algebra/tensor_product): Remove the priorities from the module structure (#5667)
  chore(category_theory/limits/over): generalise, golf and document over limits (#5674)
  chore(scripts): update nolints.txt (#5705)
  feat(measure_theory/pi): `ae_eq` lemmas about intervals in `Π i, α i` (#5633)
  feat(algebra/splitting_field): Restrict to splitting field (#5562)
  chore(scripts): update nolints.txt (#5699)
  feat(analysis/special/functions/trigonometric): complex trig and some even/odd lemmas (#5404)
  feat(equiv|set|topology): various additions (#5656)
  chore(measure_theory/set_integral): use weaker assumptions here and there (#5647)
  feat(field_theory/separable): Remove hypothesis in irreducible.separable (#5687)
  feat(order/complete_well_founded): characterise well-foundedness for complete lattices (#5575)
  chore(order/filter): a few more lemmas about `eventually` and set operations (#5686)
  chore(order/filter/basic): a few `simp` lemmas (#5685)
  feat(data/equiv/basic, logic/embedding): swap commutes with injective functions (#5636)
  chore(scripts): update nolints.txt (#5682)
  feat(algebra/lie/basic): Lie ideal operations are linear spans (#5676)
  feat(measure_theory/lp_space): add more lemmas about snorm (#5644)
  chore(data/set/lattice): add a few simp lemmas (#5671)
  feat(topology/separation, topology/metric_space/basic): add lemmas on discrete subsets of a topological space (#5523)
  feat(topology/algebra/ordered): prove `tendsto.Icc` for pi-types (#5639)
  chore(scripts): update nolints.txt (#5673)
  feat(category_theory/limits): preserving pullbacks (#5668)
  chore(linear_algebra/alternating): golf a proof (#5666)
  chore(algebra/group/hom): fix additive version of docstring (#5660)
  chore(analysis/special_functions/trigonometric): adding `@[pp_nodot]` to complex.log (#5670)
  feat(data/finset/intervals, data/set/intervals/basic): intersection of finset.Ico, union of intervals for sets and finsets (#5410)
  feat(algebra/linear_ordered_comm_group_with_zero): Add linear_ordered_comm_monoid_with_zero and an instance for nat (#5645)
  feat(geometry/manifold/times_cont_mdiff): API for checking `times_cont_mdiff` (#5631)
  feat(category_theory/closed): Frobenius reciprocity of cartesian closed categories (#5624)
  feat(measure_theory/measure_space): ae_measurable and measurable are equivalent for complete measures (#5643)
  refactor(linear_algebra/alternating): Use unapplied maps when possible (#5648)
  chore(algebra/ordered_monoid): rename lemmas (#5657)
  feat(measure_theory/borel_space): locally finite measure is sigma finite (#5634)
  refactor(algebra/module/basic): Clean up all the nat/int semimodule definitions (#5654)
  feat(topology/algebra): add additive/multiplicative instances (#5662)
  chore(scripts): update nolints.txt (#5661)
  feat(measure_theory): some additions (#5653)
  chore(data/list/basic): tag mmap(') with simp (#5443)
  feat(category_theory/sites): category of sheaves on the trivial topology  (#5651)
  feat(category_theory/monad): reflector preserves terminal object (#5649)
  feat(measure_theory/borel_space): a compact set has finite measure (#5628)
  feat(category_theory/closed): golf definition and proofs (#5623)
  feat(category_theory/limits): the product comparison natural transformation (#5621)
  ...
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin approved these changes

@kbuzzard kbuzzard Awaiting requested review from kbuzzard

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@eric-wieser @jcommelin