_p_imp_submul

Definition

by Baitian · May 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

small importer probe

Definition code

import Definitions.Def_asym_spec_Submultiplicative

def _p_imp_submul : Nat := 0