We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
FrobeniusRiou.lean
1 parent 66eeb47 commit 556ddd0Copy full SHA for 556ddd0
FLT/MathlibExperiments/FrobeniusRiou.lean
@@ -675,7 +675,7 @@ variable [Nontrivial B]
675
676
677
-- not sure if we need this but let's prove it just to check our setup is OK.
678
--- The claim is that the preimage of Q really is P (rather than just contining P)
+-- The claim is that the preimage of Q really is P (rather than just containing P)
679
-- and the proof is that A/P -> B/Q extends to a map of fields which is injective,
680
-- so A/P -> B/Q must also be injective.
681
open IsScalarTower in
0 commit comments