Post

session 9 of learning lean with @yetanotheruseless.com starting in 1 hour 🙌 7pm UTC last week we defined what subgroups are, and proved that a set consisting of just the identity value is a perfectly valid subgroup!

aron@adler.dev

session 8 of learning lean with @yetanotheruseless.com starting in 45m! we're going to prove some algebra theorems yo

27/7/26, 5:59 pm1 repost6 likes

aron

@adler.dev

27 July

today we're going to define Normal subgroups and prove the relationship between them and homomorphisms ✨ see it live at twitch.tv/aronadler

Neq

@nequals001.bsky.social

27 July

apologies for the backseat driving, i was TheMathmanProphecies, have a good night!

aron

@adler.dev

27 July

ahahaha thanks for joining dude! 🥰 you made it a lot of fun istg once i've gotten some sleep i *will* be able to figure this shit out 😤 brain had turned to absolute mush by this point

Neq

@nequals001.bsky.social

27 July

oh yeah for sure, it'll make more sense after some rest. it's all identity pushing anyway, it's just figuring out what BS you're trying to accomplish, and what are the legal moves you're allowed to make

aron

@adler.dev

27 July

github.com/Arrow7000/le...

github.comAAAAAHHH my kingdom for a non-cancelled inverse 🫠 · Arrow7000/lean-streaming@cf4cd8e