Commit 2018-09-18 13:08 a72807fa

View on Github →

feat(ring_theory/matrix): (finally!) adding matrices (#334) Joint work by: Ellen Arlt, Blair Shi, Sean Leather, Scott Morrison, Johan Commelin, Kenny Lau, Johannes Hölzl, Mario Carneiro

Estimated changes

Created ring_theory/matrix.lean

added theorem matrix.add_mul

added theorem matrix.add_val

added theorem matrix.ext

added theorem matrix.ext_iff

added theorem matrix.mul_add

added theorem matrix.mul_val'

added theorem matrix.mul_val

added theorem matrix.mul_zero

added theorem matrix.neg_val

added theorem matrix.one_val

added theorem matrix.one_val_eq

added theorem matrix.one_val_ne'

added theorem matrix.one_val_ne

added theorem matrix.zero_mul

added theorem matrix.zero_val

added def matrix