Skip to content

Commit

Permalink
make CI happy
Browse files Browse the repository at this point in the history
  • Loading branch information
Tragicus committed Aug 1, 2024
1 parent 660c747 commit f110da7
Showing 1 changed file with 5 additions and 5 deletions.
10 changes: 5 additions & 5 deletions auxresults.v
Original file line number Diff line number Diff line change
Expand Up @@ -1477,16 +1477,16 @@ Proof. by rewrite mulrC modp_mul mulrC. Qed.

End AuxiliaryResults.

Section InjectiveTheory.

Lemma raddf_inj (R S : zmodType) (f : {additive R -> S}) :
(forall x, f x = 0 -> x = 0) -> injective f.
Proof.
move=> f_inj x y /eqP; rewrite -subr_eq0 -raddfB => /eqP /f_inj /eqP.
by rewrite subr_eq0 => /eqP.
Qed.

(*Variable (R S : ringType) (f : {injmorphism R -> S}).
(* Section InjectiveTheory.
Variable (R S : ringType) (f : {injmorphism R -> S}).
Lemma rmorph_inj : injective f. Proof. by case: f => [? []]. Qed.
Expand All @@ -1503,9 +1503,9 @@ by rewrite !coef_map => /rmorph_inj.
Qed.
Canonical map_poly_is_injective := InjMorphism map_poly_injective.
*)
End InjectiveTheory.
(* Hint Resolve rmorph_inj.
Hint Resolve rmorph_inj.
Canonical polyC_is_injective (R : ringType) := InjMorphism (@polyC_inj R).
Expand Down

0 comments on commit f110da7

Please sign in to comment.