R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
⊢ False
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
⊢ Nontrivial R
by_contra h
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
⊢ (Fin 0 → R) ≃ₗ[R] Fin 1 → R
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
⊢ False
refine' zero_ne_one (eq_of_fin_equiv R _)
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
this : Subsingleton R
⊢ (Fin 0 → R) ≃ₗ[R] Fin 1 → R
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
⊢ (Fin 0 → R) ≃ₗ[R] Fin 1 → R
haveI := not_nontrivial_iff_subsingleton.1 h
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
this✝ : Subsingleton R
this : Subsingleton (Fin 1 → R)
⊢ (Fin 0 → R) ≃ₗ[R] Fin 1 → R
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
this : Subsingleton R
⊢ (Fin 0 → R) ≃ₗ[R] Fin 1 → R
haveI : Subsingleton (Fin 1 → R) :=
  Subsingleton.intro <| fun a b => funext fun x => Subsingleton.elim _ _
no goals
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
this✝ : Subsingleton R
this : Subsingleton (Fin 1 → R)
⊢ (Fin 0 → R) ≃ₗ[R] Fin 1 → R
exact
  { toFun := 0
    invFun := 0
    map_add' := by aesop
    map_smul' := by aesop
    left_inv := fun _ => by simp
    right_inv := fun _ => by simp }
no goals
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
this✝ : Subsingleton R
this : Subsingleton (Fin 1 → R)
⊢ ∀ (x y : Fin 0 → R), OfNat.ofNat 0 (x + y) = OfNat.ofNat 0 x + OfNat.ofNat 0 y
aesop
no goals
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
this✝ : Subsingleton R
this : Subsingleton (Fin 1 → R)
⊢ ∀ (r : R) (x : Fin 0 → R),
    AddHom.toFun { toFun := 0, map_add' := (_ : ∀ (x y : Fin 0 → R), OfNat.ofNat 0 (x + y) = 0 + 0) } (r • x) =
      ↑(RingHom.id R) r •
        AddHom.toFun { toFun := 0, map_add' := (_ : ∀ (x y : Fin 0 → R), OfNat.ofNat 0 (x + y) = 0 + 0) } x
aesop
no goals
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
this✝ : Subsingleton R
this : Subsingleton (Fin 1 → R)
x✝ : Fin 0 → R
⊢ OfNat.ofNat 0
      (AddHom.toFun
        { toAddHom := { toFun := 0, map_add' := (_ : ∀ (x y : Fin 0 → R), OfNat.ofNat 0 (x + y) = 0 + 0) },
            map_smul' := (_ : ∀ (r : R) (x : Fin 0 → R), OfNat.ofNat 0 (r • x) = r • 0) }.toAddHom
        x✝) =
    x✝
simp
no goals
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
this✝ : Subsingleton R
this : Subsingleton (Fin 1 → R)
x✝ : Fin 1 → R
⊢ AddHom.toFun
      { toAddHom := { toFun := 0, map_add' := (_ : ∀ (x y : Fin 0 → R), OfNat.ofNat 0 (x + y) = 0 + 0) },
          map_smul' := (_ : ∀ (r : R) (x : Fin 0 → R), OfNat.ofNat 0 (r • x) = r • 0) }.toAddHom
      (OfNat.ofNat 0 x✝) =
    x✝
simp