@[reducible, inline]

abbrev O : Type

Equations

• O = (T → ℝ>0)

structure Γ : Type

• atoms : S₀
• mints : S₁
• amms : AMMs

theorem Γ.eq_iff (s s' : Γ) : s = s' ↔ s.atoms = s'.atoms ∧ s.mints = s'.mints ∧ s.amms = s'.amms