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.

Estimated changes