mathlib3
d06b11a5 - refactor(algebra/lie/basic): golf `lie_algebra.morphism.map_bot_iff` (#6114)

Commit
5 years ago
refactor(algebra/lie/basic): golf `lie_algebra.morphism.map_bot_iff` (#6114) Co-authors: `lean-gptf`, Stanislas Polu This was found by `formal-lean-wm-to-tt-m1-m2-v4-c4` when we evaluated it on theorems added to `mathlib` after we last extracted training data. Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Author
Jesse Michael Han
Parents
Loading