pith. machine review for the scientific record. sign in
theorem proved tactic proof

plotEncoding_image_eq_nonzero

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 163theorem plotEncoding_image_eq_nonzero :
 164    Finset.univ.image plotEncoding =
 165      Finset.univ.filter (fun v : F2Power 3 => v ≠ 0) := by

proof body

Tactic-mode proof.

 166  apply Finset.eq_of_subset_of_card_le
 167  · intro v hv
 168    rcases Finset.mem_image.mp hv with ⟨p, _, hp⟩
 169    rw [Finset.mem_filter, ← hp]
 170    exact ⟨Finset.mem_univ _, plotEncoding_image_nonzero p⟩
 171  · rw [F2Power.nonzero_card_three]
 172    have : (Finset.univ.image plotEncoding).card =
 173           Fintype.card BookerPlotFamily := by
 174      rw [Finset.card_image_of_injective _ plotEncoding_injective]
 175      rfl
 176    rw [this, BookerPlotFamily.card_eq_seven]
 177
 178/-! ## §3. The count theorem (replaces the asserted `:= 7`) -/
 179
 180/-- The number of non-trivial 1-dimensional subgroups of
 181    `Q₃ = F2Power 3` is `2 ^ 3 - 1 = 7`. This is the actual count
 182    theorem, chained off `F2Power.nonzero_card_three`. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (16)

Lean names referenced from this declaration's body.