Prove2Me

The Lean 4 theorem `reduce_generator_mul_m` in the `ChapterH6` chapter of the timepiece formalization

Proved
BookProof.ChapterH6.reduce_generator_mul_m

by leonardopedro · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

timepiece

The Lean 4 theorem reduce_generator_mul_m in the ChapterH6 chapter of the timepiece formalization.

Preamble
-- Generated from ChapterH6.lean — theorem BookProof.ChapterH6.reduce_generator_mul_m
import Mathlib
import Definitions.Def_ChapterH6
open BookProof.ChapterH6


noncomputable section

open Filter Topology
Formal statement
theorem BookProof.ChapterH6.reduce_generator_mul_m (m : ℕ) : Fintype.card (Fin m × Fin m) = m * m := by sorry
Source
https://github.com/leonardopedro/timepiece/blob/61595bc/BookProof/ChapterH6.lean

View graph