feat(algebra/free_algebra): Add a nontrivial instance (#5033)

src/algebra/free_algebra.lean

@@ -6,6 +6,7 @@ Author: Scott Morrison, Adam Topaz.
 import algebra.algebra.subalgebra
 import algebra.monoid_algebra
 import linear_algebra
+import data.equiv.transfer_instance
 
 /-!
 # Free Algebras
@@ -314,6 +315,9 @@ begin
 end
 (by { ext, simp, })
 
+instance [nontrivial R] : nontrivial (free_algebra R X) :=
+equiv_monoid_algebra_free_monoid.to_equiv.nontrivial
+
 end free_algebra
 
 -- There is something weird in the above namespace that breaks the typeclass resolution of `has_coe_to_sort` below.