nontrivial_of_invariantBasisNumber

English

Any nontrivial invariant-basis-number ring is nontrivial; in particular, 0 ≠ 1 holds in such a ring.

Русский

Любое нетривиальное кольцо с отсутствием инвариантной базисной размерности должно удовлетворять 0 ≠ 1; то есть кольцо не тривиально.

LaTeX

$$If R is a ring with InvariantBasisNumber, then Nontrivial R holds, i.e. 0 ≠ 1.$$

Lean4

theorem nontrivial_of_invariantBasisNumber : Nontrivial R :=
  by
  by_contra! h
  refine zero_ne_one (eq_of_fin_equiv R ?_)
  haveI : Subsingleton (Fin 1 → R) := Subsingleton.intro fun a b => funext fun x => Subsingleton.elim _ _
  exact
    { toFun := 0
      invFun := 0
      map_add' := by simp
      map_smul' := by simp
      left_inv := fun _ => by simp [eq_iff_true_of_subsingleton]
      right_inv := fun _ => by simp [eq_iff_true_of_subsingleton] }

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