diff options
| author | Cyril Cohen | 2019-09-24 14:27:41 +0200 |
|---|---|---|
| committer | GitHub | 2019-09-24 14:27:41 +0200 |
| commit | 50856f013e47c6469bb9c05300c48d94db121195 (patch) | |
| tree | a2f351db4fe1d5ad2e27b3d15a7fe65589ab615a /mathcomp | |
| parent | fe30314bc728339353a9a4e490c8aedc61287752 (diff) | |
| parent | 3ad8a9418dc5d39ef553033f5c8f581525a3aae3 (diff) | |
Merge pull request #380 from pi8027/ring-core-scope
Fix a typo: `ring_core_scope`
Diffstat (limited to 'mathcomp')
| -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. |