diff options
| author | Kazuhiko Sakaguchi | 2019-09-03 16:31:29 +0200 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2019-09-18 10:13:31 +0200 |
| commit | 3ad8a9418dc5d39ef553033f5c8f581525a3aae3 (patch) | |
| tree | a2f351db4fe1d5ad2e27b3d15a7fe65589ab615a /mathcomp/algebra | |
| parent | fe30314bc728339353a9a4e490c8aedc61287752 (diff) | |
Fix a typo: ring_core_scope -> ring_scope
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 12fcecb..dd84f31 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -4398,7 +4398,7 @@ by move/(order_path_min argCle_trans)/allP->. Qed. Definition nthroot n x := let: RootCspec y _ _ := rootC_subproof n x in y. -Notation "n .-root" := (nthroot n) (at level 2, format "n .-root") : ring_core_scope. +Notation "n .-root" := (nthroot n) (at level 2, format "n .-root") : ring_scope. Notation "n .-root" := (nthroot n) (only parsing) : ring_scope. Notation sqrtC := 2.-root. |