search

hhu-adam / Robo

A game for learning lean 4 where a cute little Robo joins you on your exploration of the Mathiverse. The game is in German 🇩🇪
https://adam.math.hhu.de
Apache License 2.0
16 stars 9 forks source link

Fix typo in L11_SSubset.lean #13

Closed tautastic closed 4 months ago

joneugster commented 4 months ago

Danke! Muss ich mal besprechen, ob es da eine Meinung gibt. Laut Duden ist benützen korrekt. Würde dann mit Search&Replace alle in die eine oder andere Richtung ändern, wenn sich unsere Gruppe klar gegen Süddeutsche Rechtschreibung ausspricht :)