290 Formalization

9 Algebra