Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_localized_module.mk_of_algebra

Modification history

2022-12-07 08:32

src/algebra/module/localized_module.lean

feat(algebraic_geometry/Spec): `(f∗ 𝒪ₛ)ₚ` is just the localization `Sₚ` for affine `f : Spec S ⟶ Spec R` (#17471)

Added is_localized_module.mk_of_algebra View on Github →