We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 1524a05 commit 540b1dfCopy full SHA for 540b1df
classical/functions.v
@@ -2680,12 +2680,12 @@ Proof. by apply/funext => x/=; rewrite mulrC. Qed.
2680
Lemma min_fun_to_max (T : Type) (T' : numDomainType) (f g : T -> T') :
2681
(f \min g) = (f + g) - (f \max g).
2682
Proof.
2683
-apply/funext=> x /=; by rewrite minr_to_max. Qed.
+apply/funext=> x /=; by rewrite Num.Theory.minr_to_max. Qed.
2684
2685
Lemma max_fun_to_min (T : Type) (T' : numDomainType) (f g : T -> T') :
2686
(f \max g) = (f + g) - (f \min g).
2687
2688
-apply/funext => x /=; by rewrite maxr_to_min. Qed.
+apply/funext => x /=; by rewrite Num.Theory.maxr_to_min. Qed.
2689
2690
Lemma fun_maxC d (T : Type) (T' : orderType d) (f g : T -> T') :
2691
f \max g = g \max f.
0 commit comments