ofBijectiveAlgebraMap_dimension — Mathlib

English

If the algebra map is bijective, the associated presentation has dimension zero.

Русский

Если отображение биективно, связанная презентация имеет размерность равную нулю.

LaTeX

$$$\\mathrm{ofBijectiveAlgebraMap}\\ h\\ ;\\mathrm{dimension} = 0$$$

Lean4

theorem ofBijectiveAlgebraMap_dimension (h : Function.Bijective (algebraMap R S)) :
    (ofBijectiveAlgebraMap h).dimension = 0 := by simp [dimension]

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