Understanding \is a unit in ssreflect

Question

I'm really annoyed by the following goal:

a%:R \is a unit

where a is a nat. The only lemma that seems to help is unitrE, but then it seems impossible to simplify further. This goal should be solvable. Can someone explain how to coerce this to a field type so I can use unitfE which I can easily work with.

Answer 1

you can only use unitfE if the structure you work with is a field. Otherwise you need to deal with the characteristic ([char R]) of your ring. What is your structure?

Answer 2

If you assume that a is non-zero (which makes sense, to have an inverse), then you can do this:

From mathcomp Require Import all_ssreflect all_algebra.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Open Scope ring_scope.
Import GRing.Theory.

Variable (R : numFieldType).

Variable (a : nat).

Definition a' : R := a%:R.

Hypothesis nea'0 : a' != 0.

Lemma a'unit : a' \is a GRing.unit.
Proof. by rewrite unitfE nea'0. Qed.