kronecker_delta_comm@{} (i j : A) (r : R) : r * kronecker_delta i j = kronecker_delta i j * r. Proof. unfold kronecker_delta. destruct (dec (i = j)). - exact (rng_mult_one_r _ @ (rng_mult_one_l _)^). - exact (rng_mult_zero_r _ @ (rng_mult_zero_l _)^). Defined.
Require Import Basics.Overture Basics.Decidable Spaces.Nat. Require Import Algebra.Rings.Ring. Require Import Classes.interfaces.abstract_algebra.