The quantity model identifies coherent units faithfully

import Mathlib
import Definitions.Def_SI_dim
import Definitions.Def_SI_units
import Definitions.Def_SI_qmodel

/-!
# The quantity model identifies coherent units faithfully

The seven value postulates of Table 1, together with the
unimodularity of the dimension-exponent matrix of the defining
constants, determine the exponent assignment of every quantity model
of the SI: it is the inverse of the dimension map. Consequently the
identification of a coherent unit with its defining-constant monomial
is faithful: two coherent units denoting the same quantity of the
defining constants have the same dimension and the same numerical
factor, hence are the same unit. This is the formal content of the
statement of section 2.2 that the seven defining constants, together
with the definitions of the units in which they are expressed, fix the
complete system. This milestone is proved on the way to the goal
theorem `SI.si_complete`.
-/

namespace SI

/-- In every quantity model of the SI whose dimension map dimOfExpo is
bijective (milestone `SI.dim_basis`), the map identifying a coherent
unit with its defining-constant monomial is injective on coherent
units: two coherent units with the same image are equal. -/
theorem model_faithful (M : SIModel)
    (hbas : Function.Bijective dimOfExpo) :
    ∀ u v : SIUnit, IsCoherent u → IsCoherent v →
      toQ M u = toQ M v → u = v := by
  sorry

end SI