lean-test-2 Learning lean4 and dependent types by proving random facts without mathlib: Contains proof that multiplication of polynomials over commutative Ring is commutative.
