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.
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
[Merged by Bors] - feat: port Data.Multiset.Basic #1491
Conversation
jcommelin
commented
Jan 11, 2023
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Mathlib/Data/Multiset/Basic.lean
Outdated
decreasing_by exact card_lt_of_lt _h | ||
#align multiset.strong_induction_on Multiset.strongInductionOnₓ -- Porting note: reorderd universes | ||
|
||
theorem strong_induction_eq {p : Multiset α → Sort _} (s : Multiset α) (H) : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What should this be called? Maybe strongInductionOn_eq
would make more sense
Mathlib/Data/Multiset/Basic.lean
Outdated
end | ||
|
||
@[ext] | ||
theorem add_hom_ext [AddZeroClass β] ⦃f g : Multiset α →+ β⦄ (h : ∀ x, f {x} = g {x}) : f = g := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
addHom_ext
?
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
bors r+ |
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Reid Barton <rwbarton@gmail.com> Co-authored-by: qawbecrdtey <qawbecrdtey@kaist.ac.kr> Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded:
|
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Reid Barton <rwbarton@gmail.com> Co-authored-by: qawbecrdtey <qawbecrdtey@kaist.ac.kr> Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>