mathlib
8aadbcb7 - feat(linear_algebra/*_algebra): add some simp lemmas about the algebra map and generators of free constructions (#10247)

Commit

4 years ago

feat(linear_algebra/*_algebra): add some simp lemmas about the algebra map and generators of free constructions (#10247) These are quite repetitive, but I'm not sure how to generalize

Author

eric-wieser

Parents

543fcef1

mathlib 8aadbcb7 - feat(linear_algebra/*_algebra): add some simp lemmas about the algebra map and generators of free constructions (#10247)

mathlib
8aadbcb7 - feat(linear_algebra/*_algebra): add some simp lemmas about the algebra map and generators of free constructions (#10247)