mathlib3
Def h spaces
#16400
Merged
Overview
Commits
5
Changes
View On GitHub

Def h spaces #16400

faenuccio merged 5 commits into leanprover-community:def_H_spaces from alreadydone:def_H_spaces
faenuccio
alreadydone golf with new Q_right
8ff63234
alreadydone tiny golf
1998c371
alreadydone comment
af1a2949
alreadydone left/right_Hmul_e: reverse order
a2b902f4
alreadydone remove unnecessary delayed_refl_right_e, golf
8466579c
faenuccio faenuccio merged d9889c8b into def_H_spaces 3 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum