We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent a66f1d6 commit 2d0b331Copy full SHA for 2d0b331
1 file changed
Mathlib/RingTheory/FractionalIdeal/Operations.lean
@@ -916,7 +916,7 @@ variable {R S : Type*} (K L : Type*) [CommRing R] [IsDomain R] [CommRing S] [IsD
916
local instance (f : R ≃+* S) : RingHomInvPair (f : R →+* S) f.symm :=
917
RingHomInvPair.of_ringEquiv f
918
919
-/-- If `f : R →+* S` is a ring isomorphism and `I : Submodule R K` is fractional with respect to
+/-- If `f : R ≃+* S` is a ring isomorphism and `I : Submodule R K` is fractional with respect to
920
`R⁰`, then `I.map (IsFractionRing.semilinearEquivOfRingEquiv K L f).toLinearMap`
921
is fractional with respect to `S⁰`.
922
0 commit comments