We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 06a46da commit 83e7c54Copy full SHA for 83e7c54
1 file changed
Counterexamples/InvertibleModuleNotIdeal.lean
@@ -33,7 +33,6 @@ instance : IsFractionRing (SqZeroExtQuotMax R) (SqZeroExtQuotMax R) :=
33
/-- R as an algebra over `SqZeroExtQuotMax R`. -/
34
abbrev SqZeroExtQuotMax.algebraBase : Algebra (SqZeroExtQuotMax R) R := TrivSqZeroExt.algebraBase ..
35
36
-#adaptation_note /-- After nightly-2026-02-23 we need this to avoid timeouts. -/
37
open CommRing (Pic) in
38
/-- If the Picard group of a commutative ring R is nontrivial, then `SqZeroExtQuotMax R`
39
has an invertible module (which is the base change of an invertible ideal of R)
0 commit comments