Yama2026_Sections_1_And_2_1.lean
1import Yama2026_Sections_1_And_2_1.main 4# Yama2026 Sections 1 and 2.1 6Public root module for the formalized Section 1 and Subsection 2.1 material. 7The declarations themselves live in 8`Yama2026_Sections_1_And_2_1.main`.