Skip to content

Commit

Permalink
Update GaloisRamification/ToMathlib/IsGalois.lean
Browse files Browse the repository at this point in the history
Co-authored-by: Yongle Hu <[email protected]>
  • Loading branch information
yhtq and mbkybky authored Oct 29, 2024
1 parent ca817c6 commit e54e3cf
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion GaloisRamification/ToMathlib/IsGalois.lean
Original file line number Diff line number Diff line change
Expand Up @@ -108,7 +108,7 @@ end

/- Galois extension is transfered between two pairs of fraction rings
-/
theorem IsGalois.of_isGalois_isfractionRing
theorem IsGalois.of_isGalois_isFractionRing
(A B K L K' L' : Type*)
[CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [Algebra A B] [NoZeroSMulDivisors A B]
[Field K] [Field L]
Expand Down

0 comments on commit e54e3cf

Please sign in to comment.