upper_triangular_matrix_ring@{i} (R : Ring@{i}) (n : nat) : Subring@{i i} (matrix_ring@{i} R n). Proof. nrapply (Build_Subring' (fun M : matrix_ring R n => IsUpperTriangular M)). - exact _. - intros x y ? ?; exact (upper_triangular_plus x (-y)). - exact upper_triangular_mult. - exact upper_triangular_identity. 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.