Basic_Results_about_Unitary_Modules
Provedbasic-resultsmodule-theoryproofwikiunitary-modules
Let be an abelian group whose identity is . Let be a ring with unity whose zero is and whose unity is . Let be an unitary -module. Let . Then
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Basic_Results_about_Unitary_Modules {R : Type _} [Ring R] {M : Type _} [AddCommGroup M] [Module R M] (m : M) : (1 : R) • m = m := by sorrySource