q : ℕ+
w : 1 < q
this : Fact (1 < ↑q)
⊢ Fintype.card (X q)ˣ < ↑q ^ 2
q : ℕ+
w : 1 < q
⊢ Fintype.card (X q)ˣ < ↑q ^ 2
have : Fact (1 < (q : ℕ)) := ⟨w⟩
case h.e'_4
q : ℕ+
w : 1 < q
this : Fact (1 < ↑q)
⊢ ↑q ^ 2 = Fintype.card (X q)
q : ℕ+
w : 1 < q
this : Fact (1 < ↑q)
⊢ Fintype.card (X q)ˣ < ↑q ^ 2
convert card_units_lt (X q)
no goals
case h.e'_4
q : ℕ+
w : 1 < q
this : Fact (1 < ↑q)
⊢ ↑q ^ 2 = Fintype.card (X q)
rw [card_eq]