matrix_diag_ring@{i} (R : Ring@{i}) (n : nat) : Subring@{i i} (matrix_ring R n). Proof. snrapply (Build_Subring' (fun M : matrix_ring R n => IsDiagonal M) _); hnf. - intros; exact _. - intros x y dx dy. nrapply isdiagonal_matrix_plus; trivial. by nrapply isdiagonal_matrix_negate. - nrapply isdiagonal_matrix_mult. - nrapply isdiagonal_identity_matrix. Defined.
Require Import Basics.Overture Basics.Trunc Basics.Tactics Basics.Decidable. Require Import Types.Sigma. Require Import Spaces.List.Core Spaces.List.Theory Spaces.List.Paths. Require Import Algebra.Rings.Ring Algebra.Rings.Module Algebra.Rings.CRing Require Import abstract_algebra. Require Import WildCat.Core WildCat.Paths. Require Import Modalities.ReflectiveSubuniverse.