Commit 2025-08-14 13:06 9b32ba19
View on Github →feat(Subalgebra): simp lemma for algebraMap mk (#27637)
Add three lemma (two simp) for the interaction of Subalgebra.mk
and algebraMap
.
Let me know if you think these lemmas should be placed elsewhere.