English
The collection CharacterModule A carries a FunLike structure from A to AddCircle(1).
Русский
Множество CharacterModule A обладает структурой FunLike от A к AddCircle(1).
LaTeX
$$$$ \\text{CharacterModule } A \\ \\, \\text{is a FunLike from } A \\text{ to } \\mathrm{AddCircle}(1). $$$$
Lean4
/-- The cardinality of a nontrivial module over a ring is at least the cardinality of the ring if
there are no zero divisors (for instance if the ring is a field) -/
theorem mk_le_of_module (R : Type u) (E : Type v) [AddCommGroup E] [Ring R] [Module R E] [Nontrivial E]
[NoZeroSMulDivisors R E] : Cardinal.lift.{v} (#R) ≤ Cardinal.lift.{u} (#E) :=
by
obtain ⟨x, hx⟩ : ∃ (x : E), x ≠ 0 := exists_ne 0
have : Injective (fun k ↦ k • x) := smul_left_injective R hx
exact lift_mk_le_lift_mk_of_injective this
