NYLL
Module

FreeModuleRegularScalar.lean

Nyll.SchemeTheory.RingTheory.FreeModuleRegularScalar
1 declaration indexed from sourceView source ↗

Module documentation

Regular scalar multiplication on a nontrivial free module

Scalar multiplication by a ring element is injective on a nontrivial free module exactly when multiplication by that element is injective on the ring.

Imports3
  • Mathlib.Algebra.Regular.SMul
  • Mathlib.LinearAlgebra.FreeModule.Basic
  • Mathlib.Tactic.Ext
Imported by2

Declarations

theorem

isSMulRegular_iff_of_free

L29 ↗
Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.isSMulRegular_iff_of_free
Lean source · statement
theorem _root_.isSMulRegular_iff_of_free {R M : Type*} [CommRing R]
    [AddCommGroup M] [Module R M] [Module.Free R M] [Nontrivial M] {r : R} :
    IsSMulRegular M r ↔ IsSMulRegular R r

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.