Skip to content

Commit 1a4917a

Browse files
committed
doc(Logic/Basic): fix mathlib3 name in doc-string (#38791)
1 parent 33246d8 commit 1a4917a

1 file changed

Lines changed: 4 additions & 4 deletions

File tree

Mathlib/Logic/Basic.lean

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -83,11 +83,11 @@ in specific circumstances.
8383
8484
For example, `ZMod p` is a field if and only if `p` is a prime number.
8585
In order to be able to find this field instance automatically by type class search,
86-
we have to turn `p.prime` into an instance implicit assumption.
86+
we have to turn `p.Prime` into an instance implicit assumption.
8787
88-
On the other hand, making `Nat.prime` a class would require a major refactoring of the library,
89-
and it is questionable whether making `Nat.prime` a class is desirable at all.
90-
The compromise is to add the assumption `[Fact p.prime]` to `ZMod.field`.
88+
On the other hand, making `Nat.Prime` a class would require a major refactoring of the library,
89+
and it is questionable whether making `Nat.Prime` a class is desirable at all.
90+
The compromise is to add the assumption `[Fact p.Prime]` to `ZMod.instField`.
9191
9292
In particular, this class is not intended for turning the type class system
9393
into an automated theorem prover for first-order logic. -/

0 commit comments

Comments
 (0)