relIndex_ne_zero_trans — Mathlib

English

Let f be a group homomorphism. If J.relIndex K ≠ 0, then the relative index of the preimages under f is also nonzero.

Русский

Пусть f — гомоморфизм. Если J.relIndex K ≠ 0, то относительный индекс прообразов через f также не равен нулю.

LaTeX

$$$\text{If } J.\relIndex K \neq 0 \text{ then } (J \comap f).\relIndex (K \comap f) \neq 0$$$

Lean4

@[to_additive]
theorem relIndex_ne_zero_trans (hHK : H.relIndex K ≠ 0) (hKL : K.relIndex L ≠ 0) : H.relIndex L ≠ 0 := fun h =>
  mul_ne_zero (mt (relIndex_eq_zero_of_le_right (show K ⊓ L ≤ K from inf_le_left)) hHK) hKL
    ((relIndex_inf_mul_relIndex H K L).trans (relIndex_eq_zero_of_le_left inf_le_left h))

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