card_le_card_mul_left_of_injective

English

If a ∈ s and the map x ↦ a * x is injective, then #t ≤ #(s * t).

Русский

Если a ∈ s и отображение x ↦ a*x инъективно, то размерность (#t) не превышает #(s*t).

LaTeX

$$(has : a ∈ s) (ha : Function.Injective (a * ·)) : #t ≤ #(s * t)$$

Lean4

/-- See `card_le_card_mul_left` for a more convenient but less general version for types with a
left-cancellative multiplication.
-/
@[to_additive /-- See `card_le_card_add_left` for a more convenient but less general version for types with a
    left-cancellative addition. -/
    ]
theorem card_le_card_mul_left_of_injective (has : a ∈ s) (ha : Function.Injective (a * ·)) : #t ≤ #(s * t) :=
  card_le_card_image₂_left _ has ha

Похожие утверждения