Stream: new members
I have some algebraic structure, say a vector space. Then I take a quotient on the structure, and the equivalence relation is respected by all the operations of the algebraic structure (like addition and scalar multiplication). Then I want to say that the quotient space has the same algebraic structure, and there is a natural homomorphism between the original space and the quotient space. Do I need to prove everything again?
Patrick Massot (Mar 11 2019 at 20:25):
Currently we don't have a tactic automating this. But there are many examples in mathlib (including the one of vector spaces).
Last updated: May 12 2021 at 23:13 UTC