theorem
L30 ↗isWeaklyRegular_of_free
RingTheory.Sequence.isWeaklyRegular_of_free
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace RingTheory_Sequence_isWeaklyRegular_of_free
open scoped Pointwise TensorProductLean source · statement
theorem _root_.RingTheory.Sequence.isWeaklyRegular_of_free {R M : Type*}
[CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M]
[Nontrivial M] {s : List R} :
RingTheory.Sequence.IsWeaklyRegular M s ↔ RingTheory.Sequence.IsWeaklyRegular R s