proposition: Lemma preserves_dec_recip `{DecField F2} `{∀ x y: F2, Decision (x = y)} `{!SemiRing_Morphism (f : F → F2)} x : f (/ x) = / f x.
proof: Proof. case (decide (x = 0)) as [E | E]. now rewrite E, dec_recip_0, preserves_0, dec_recip_0. intros. apply (left_cancellation_ne_0 (.*.) (f x)). now apply injective_ne_0. rewrite <-preserves_mult, 2!dec_recip_inverse. now apply preserves_1. now apply injective_ne_0. easy. Qed.
imports: Coq.setoid_ring.Field Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.vectorspace MathClasses.theory.fields MathClasses.theory.strong_setoids MathClasses.theory.rings