Commit 2023-02-18 20:01 7e1713a1

feat: port LinearAlgebra.Quotient (#2286) porting notes:

1. Adding type ascriptions to mk or mk x and friends greatly speeds up elaboration issues.
2. What is the proper casing convention for mkq or liftq (and variants). Is is mkq, or mkQ? Edit: we've gone with mkQ, liftQ and mapQ.
3. How should submodule.comap_mkq.rel_iso be called according to our naming conventions? Edit: unclear, but here it's been changed to Submodule.comapMkQRelIso.
4. Why can't Lean fill in optParams automatically in simp or rw? Edit: apparently this was never a thing in Lean 3 either.
5. Why did I need to add an optParam in Submodule.Quotient.equiv_apply that wasn't needed in Lean 3, so this has been #aligned with an ₓ, and why didn't simps generate this lemma?
6. There are some instances I feel like we may want to be default_instances, but I'm not sure. Edit: this can always be added later if necessary, so it's not urgent here. Zulip