contract_eq_contract_delete — Mathlib

English

If I is a basis' for X, then contracting X equals contracting I and deleting X \ I.

Русский

Если I является базисом' для X, то сокращение по X равно сокращению по I и удалению X \ I.

LaTeX

$$$ M ／ X = (M ／ I) \ (X \ I) $$$

Lean4

theorem contract_eq_contract_delete (hI : M.IsBasis' I X) : M ／ X = M ／ I ＼ (X \ I) := by
  rw [← contract_inter_ground_eq, hI.isBasis_inter_ground.contract_eq_contract_delete, eq_comm, ←
    delete_inter_ground_eq, contract_ground, diff_eq, diff_eq, ← inter_inter_distrib_right, ← diff_eq]

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