zmod.nat_cast_zmod_val

Stream: new members

[Thomas Laraia]

I'm trying to use this theorem:

theorem zmod.nat_cast_zmod_val {n : ℕ} [fact (0 < n)] (a : zmod n) :
↑(a.val) = a

Dose anyone understand what [fact (0<n)] means? What do the square brackets mean and how does it differ from a normal hypothesis?

I'm trying to use it with rw, but lean seems concerned that maybe 0 < n doesn't hold, but I can't seem to reassure it as usual by feeding it a proof of 0 < n.

[Johan Commelin]

@Thomas Laraia The [...] mean that Lean should use the type class system to figure out this assumption on its own.

[Johan Commelin]

What does your context look like?

[Thomas Laraia]

@Johan Commelin

lemma exist_sol_to_cong_equ_using_zmod (n a : ℕ) (h : gcd n a = 1) (onelen : 1 < n) : ∃ x : ℕ, a*x ≡ 1 [MOD n] :=
begin

  have f : (∃ x : zmod n, (a : zmod n)*x = 1) := ring_formulation n a h onelen,
  cases f with x fx,
  use x.val,
  rw ← zmod.eq_iff_modeq_nat,
  simp,
  rw zmod.nat_cast_zmod_val x,

end

[Johan Commelin]

Aha, you can add haveI : fact (0 < n) := \<zero_lt_one.trans onelen\>, above the rw.

[Thomas Laraia]

Ah cheers, what exactly does .trans do?

[Alex J. Best]

(deleted)

[Johan Commelin]

@Thomas Laraia it chains inequalities together using transitivity. (This is using so-called dot notation.)