mathlib

19f24ced - feat(algebra/subalgebra): Trivial subalgebra has trivial automorphism group (#5672)

feat(algebra/subalgebra): Trivial subalgebra has trivial automorphism group (#5672) Adds a lemma stating that if top=bot in the subalgebra type then top=bot in the subgroup type. Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>