Theory Algebra_On

(*  Title:       Algebra_On
    Author:      Richard Schmoetten <richard.schmoetten@ed.ac.uk>, 2024
    Maintainer:  Richard Schmoetten <richard.schmoetten@ed.ac.uk>
*)

theory Algebra_On
imports
  "HOL-Types_To_Sets.Linear_Algebra_On"
  "Jacobson_Basic_Algebra.Ring_Theory"
begin

section ‹Abstract algebra locales over a classfield
text ‹... with carrier set and some implicit operations
  (only algebraic multiplication, scaling, and derived constants are not implicit).›

text ‹For full generality, one could define an algebra as a ring that is also a module
  (rather than a vector space, i.e. have a (non/commutative) base ring instead of a base field).›

subsection ‹Bilinearity, Jacobi identity›


lemma (in module_hom_on) mem_hom:
  assumes "x  S1"
  shows "f x  S2"
  using scale[OF assms, of 1] m2.mem_scale[of "f x" 1] m2.scale_one_on[of "f x"] oops

locale bilinear_on =
  vector_space_pair_on V W scaleV scaleW +
  vector_space_on X scaleX
  for V:: "'b::ab_group_add set" and W::"'c::ab_group_add set" and X::"'d::ab_group_add set"
    and scaleV::"'a::field'b'b" (infixr V 75)
    and scaleW::"'a'c'c" (infixr W 75)
    and scaleX::"'a'd'd" (infixr X 75) +
  fixes f::"'b'c'd"
  assumes linearL: "wW  linear_on V X scaleV scaleX (λv. f v w)"
    and linearR: "vV  linear_on W X scaleW scaleX (λw. f v w)"
begin

lemma linearL': "vV; wW  f (a V v) w = a X (f v w)"
    "vV; v'V; wW  f (v + v') w = (f v w) + (f v' w)"
  using linearL unfolding linear_on_def module_hom_on_def module_hom_on_axioms_def
  by simp+

lemma linearR': "vV; wW  f v (a W w) = a X (f v w)"
    "vV; wW; w'W  f v (w + w') = (f v w) + (f v w')"
  using linearR unfolding linear_on_def module_hom_on_def module_hom_on_axioms_def
  by simp+

lemma bilinear_zero [simp]:
  shows "wW  f 0 w = 0" "vV  f v 0 = 0"
  using linearL'(2) m1.mem_zero linearR'(2) m2.mem_zero by fastforce+

lemma bilinear_uminus [simp]:
  assumes v: "vV" and w: "wW"
  shows "f (-v) w = - (f v w)" "f v (-w) = - (f v w)"
  using v w linearL'(2) m1.mem_uminus bilinear_zero(1) ab_left_minus add_right_imp_eq apply metis
  using v w linearR'(2) m2.mem_uminus bilinear_zero(2) add_left_cancel add.right_inverse by metis


end


text ‹For bilinear maps, "alternating" means the same as "skew-symmetric",
  which is the same as "anti-symmetric".›
locale alternating_bilinear_on = bilinear_on S S S scale scale scale f for S scale f +
  assumes alternating: "xS  f x x = 0"
begin

lemma antisym:
  assumes "xS" "yS"
  shows "(f x y) + (f y x) = 0"
proof -
  have "f (x+y) (x+y) = (f x x) + (f x y) + (f y x) + (f y y)"
    using linearL'(2) linearR'(2) by (simp add: assms m1.mem_add)
  thus ?thesis
    using alternating by (simp add: assms m1.mem_add)
qed

lemma antisym':
  assumes "xS" "yS"
  shows "(f x y) = - (f y x)"
  using antisym[OF assms] by (simp add: eq_neg_iff_add_eq_0)

lemma antisym_uminus:
  assumes "xS" "yS"
  shows "f (-x) y = f y x""f x (-y) = f y x"
  using bilinear_uminus by (metis antisym' assms)+


end


abbreviation (input) jacobi_identity_with::"'a  ('a'a'a)   ('a'a'a)  'a  'a  'a  bool"
  where "jacobi_identity_with zero_add f_add f_mult x y z 
      zero_add = f_add (f_add (f_mult x (f_mult y z)) (f_mult y (f_mult z x))) (f_mult z (f_mult x y))"

abbreviation (input) jacobi_identity::"('a::{monoid_add}'a'a)  'a  'a  'a  bool"
  where "jacobi_identity f_mult x y z  jacobi_identity_with 0 (+) f_mult x y z"

lemma (in module_hom_on) mapsto_zero: "f 0 = 0"
  using add m1.mem_zero by fastforce

lemma (in module_hom_on) mapsto_uminus: "aS1  f (-a) = - f a"
  by (metis add m1.mem_uminus neg_eq_iff_add_eq_0 mapsto_zero)

lemma (in module_hom_on) mapsto_closed: "aS1  f a  S2"
  using mapsto_zero add mapsto_uminus
oops


subsection ‹Unital and associative algebras›

locale algebra_on = bilinear_on S S S scale scale scale amult
  for S
    and scale :: "'a::field  'b::ab_group_add  'b" (infixr *S 75)
    and amult (infixr  74) +
  assumes amult_closed [simp]: "aS  bS  amult a b  S"
begin

lemma
    shows distR: "xS; yS; zS  (x+y)  z = x  z + y  z"
      and distL: "xS; yS; zS  z  (x+y) = z  x + z  y"
      and scalar_compat (* [simp] *): "xS; yS  (a *S x)  (b *S y) = (a*b) *S (x  y)"
    using algebra_on_axioms unfolding algebra_on_def bilinear_on_def bilinear_on_axioms_def
      linear_on_def module_hom_on_def module_hom_on_axioms_def
    by (blast, blast, metis m1.mem_scale m1.scale_scale_on)

  lemma scalar_compat' [simp]:
    shows "xS; yS  (a *S x)  y = a *S (x  y)"
      and "xS; yS  x  (a *S y) = a *S (x  y)"
      by (simp_all add: linearL' linearR')

end

text‹
  Sometimes an associative algebra is defined as a ring that is also a module (over a comm. ring),
  with the module and scalar multiplication being compatible, and the ring and module addition being the same.
  That definition implies an associative algebra is also unital, i.e. there is a multiplicative identity;
  in contrast, our definition doesn't. This is in agreement with how a typ'a::ring needs no identity,
  and an additional type class typ>'a::ring_1› is provided (instead of the terminology of rng vs. ring).›
locale assoc_algebra_on = algebra_on +
  assumes amult_assoc: "xS; yS; zS  (xy)z = x(yz)"


locale unital_algebra_on = algebra_on +
  fixes a_id
  assumes amult_id [simp]: "a_idS" "aS  aa_id=a" "aS  a_ida=a"
begin

  lemma id_neq_0_iff: "aS. bS. ab  0  a_id"
    using amult_id(1) m1.mem_zero by blast

  lemma id_neq_0_if:
    shows "aS  bS  ab  0  a_id"
      and "card S  2  0  a_id"
      and "infinite S  0  a_id"
  proof -

    (* Lifted from HOL-Analysis.Linear_Algebra, which I didn't want to import for one lemma. *)
    have ex_card: "SA. card S = n"
      if "n  card A"
      for n and A::"'a set"
    proof (cases "finite A")
      case True
      from ex_bij_betw_nat_finite[OF this] obtain f where f: "bij_betw f {0..<card A} A" ..
      moreover from f n  card A have "{..< n}  {..< card A}" "inj_on f {..< n}"
        by (auto simp: bij_betw_def intro: subset_inj_on)
      ultimately have "f ` {..< n}  A" "card (f ` {..< n}) = n"
        by (auto simp: bij_betw_def card_image)
      then show ?thesis by blast
    next
      case False
      with n  card A show ?thesis by force
    qed

    show "aS  bS  ab  0  a_id"
      using amult_id(2) linearR' m1.mem_zero m1.scale_zero_left by metis
    thus "card S  2  0  a_id"
      by (metis amult_id(2) card_2_iff' ex_card m1.mem_zero m1.scale_zero_left scalar_compat'(2) subset_iff)
    thus "infinite S  0  a_id"
      using infinite_arbitrarily_large
      by (metis amult_id(2) card_2_iff' linearR'(1) m1.mem_zero m1.scale_zero_left subset_iff)
  qed

  lemma id_neq_0_implies_elements (* [simp] *): "aS. bS. ab" if "0  a_id"
    using amult_id(1) m1.mem_zero that by blast

  lemma id_neq_0_implies_card:
    assumes "0  a_id"
    obtains "card S  2" | "infinite S"
    using id_neq_0_implies_elements[OF assms] unfolding numeral_2_eq_2
    using card_le_Suc0_iff_eq not_less_eq_eq by blast

  lemma id_unique [simp]:
    fixes other_id
    assumes "other_idS" "a. aS  aother_id=a  other_ida=a"
    shows "other_id = a_id"
    using assms amult_id by fastforce

end


locale assoc_algebra_1_on = assoc_algebra_on + unital_algebra_on +
  assumes id_neq_0 [simp]: "a_id  0" ― ‹this is as in the class ring_1›, and merely assures S› has at least two elements›
begin

  lemma is_ring_1_axioms:
    shows "a b c. aS  bS  cS  a  b  c = a  (b  c)"
      and "a. aS  a_id  a = a"
      and "a. aS  a  a_id = a"
      and "a b c. aS  bS  cS  (a + b)  c = a  c + b  c"
      and "a b c. aS  bS  cS  a  (b + c) = a  b + a  c"
      by (simp_all add: distR distL algebra_simps)

  lemma inverse_unique [simp]:
    assumes a: "aS" "a0"
      and x: "xS" "ax=a_id  xa=a_id"
      and y: "yS" "ay=a_id  ya=a_id"
    shows "x = y"
    using amult_assoc[of x a x] amult_assoc[of x a y]
    by (simp add: assms)

  lemma inverse_unique':
    assumes a: "aS" "a0"
      and inv_ex: "xS. ax=a_id  xa=a_id"
    shows "∃!xS. ax=a_id  xa=a_id"
    using a inv_ex inverse_unique by (metis (no_types, lifting)) 

end

lemma algebra_onI [intro]:
  fixes scale :: "'a::field  'b::ab_group_add  'b" (infixr *S 75)
    and amult (infixr  74)
  assumes "vector_space_on S scale"
    and distR: "x y z. xS; yS; zS  (x+y)  z = x  z + y  z"
    and distL: "x y z. xS; yS; zS  z  (x+y) = z  x + z  y"
    and scalar_compat: "a x y. xS; yS  (a *S x)  y = a *S (x  y)  x  (a *S y) = a *S (x  y)"
    and closure: "x y. xS; yS  x  y  S"
  shows "algebra_on S scale amult"
  unfolding algebra_on_def bilinear_on_def vector_space_pair_on_def bilinear_on_axioms_def
  apply (intro conjI algebra_on_axioms.intro, simp_all add: assms(1))
  unfolding linear_on_def module_hom_on_def module_hom_on_axioms_def
  by (auto simp: assms vector_space_on.axioms)


lemma (in vector_space_on) scalar_compat_iff:
  fixes scale_notation (infixr *S 75)
    and amult (infixr  74)
  defines "scale_notation  scale"
  assumes distR: "x y z. xS; yS; zS  (x+y)  z = x  z + y  z"
    and distL: "x y z. xS; yS; zS  z  (x+y) = z  x + z  y"
  shows "(a. xS. yS. (a *S x)  y = a *S (x  y)  x  (a *S y) = a *S (x  y)) 
      (a b. xS. yS. (a *S x)  (b *S y) = (a*b) *S (x  y))"
proof (intro iffI)
  { assume asm: "a b x y. xS  yS  a *S x  b *S y = (a * b) *S (x  y)"
    { fix a x y
      assume S: "xS" "yS"
      have "a *S x  y = a *S (x  y)" "x  a *S y = a *S (x  y)"
        using asm[of x y a 1] S apply (simp add: scale_notation_def)
        using asm[of x y 1 a] S by (simp add: scale_notation_def) }}
  thus "a b. xS. yS. a *S x  b *S y = (a * b) *S (x  y) 
      a. xS. yS. a *S x  y = a *S (x  y)  x  a *S y = a *S (x  y)"
    by blast
qed (metis mem_scale scale_notation_def scale_scale_on)


lemma (in vector_space_on) algebra_onI:
  fixes scale_notation (infixr *S 75)
    and amult (infixr  74)
  defines "scale_notation  scale"
  assumes distR: "x y z. xS; yS; zS  (x+y)  z = x  z + y  z"
    and distL: "x y z. xS; yS; zS  z  (x+y) = z  x + z  y"
    and scalar_compat: "a x y. xS; yS  (a *S x)  y = a *S (x  y)  x  (a *S y) = a *S (x  y)"
    and closure: "x y. xS; yS  x  y  S"
  shows "algebra_on S scale amult"
  using algebra_onI[of S scale amult] assms scale_notation_def vector_space_on_axioms by simp


subsection ‹Lie algebra (locale)›

text ‹
  List syntax interferes with the standard notation for the Lie bracket,
  so it can be disabled it here. Instead, we add a delimiter to the notation for Lie brackets,
  which also helps with unambiguous parsing.
›
(*no_translations
  "[x, xs]" == "x#[xs]"
  "[x]" == "x#[]"
unbundle no list_syntax and no list_enumeration_syntax
*)
(*end*)

locale lie_algebra = algebra_on 𝔤 scale lie_bracket + alternating_bilinear_on 𝔤 scale lie_bracket
  for 𝔤
    and scale :: "'a::field  'b::ab_group_add  'b" (infixr *S 75)
    and lie_bracket :: "'b  'b  'b" ([_;_] 74) +
  assumes jacobi: "x𝔤; y𝔤; z𝔤  0 = [x;[y;z]] + [y;[z;x]] + [z;[x;y]]"

lemma (in algebra_on) lie_algebraI:
  assumes alternating: "xS. amult x x = 0"
    and jacobi: "xS. yS. zS. jacobi_identity amult x y z"
  shows "lie_algebra S scale amult"
  apply unfold_locales using assms by auto

lemma (in vector_space_on) lie_algebraI:
  fixes lie_bracket :: "'b  'b  'b" ([_;_] 74)
    and scale_notation (infixr *S 75)
  defines "scale_notation  scale"
  assumes distributivity:
      "x y z. xS; yS; zS  [(x+y); z] = [x; z] + [y; z]  [z; (x+y)] = [z; x] + [z; y]"
    and scalar_compatibility:
      "a x y. xS; yS  [(a *S x); y] = a *S ([x; y])  [x; (a *S y)] = a *S ([x; y])"
    and closure: "x y. xS; yS  [x; y]  S"
    and alternating: "xS. lie_bracket x x = 0"
    and jacobi: "xS. yS. zS. jacobi_identity lie_bracket x y z"
  shows "lie_algebra S scale lie_bracket"
  using assms(1,3,6) by (auto simp: assms(2,4,5) intro!: algebra_on.lie_algebraI algebra_onI)

context lie_algebra begin

lemma jacobi_alt:
  assumes x: "x𝔤" and y: "y𝔤" and z: "z𝔤"
  shows "[x;[y;z]] = [[x;y];z] + [y;[x;z]]"
proof -
  have "[x;[y;z]] = - ([y;[z;x]]) + (- ([z;[x;y]]))"
    using jacobi[OF assms] add_implies_diff[of "[x;[y;z]]" "[y;[z;x]] + [z;[x;y]]" 0]
    by (simp add: add.commute add.left_commute)
  moreover have "[[x;y];z] = - ([z;[x;y]])" "- ([y;[z;x]]) = [y;[x;z]]"
    using antisym'[OF amult_closed[OF x y] z] antisym'[OF z x] by (simp_all add: assms)
  ultimately show "[x;[y;z]] = [[x;y];z] + [y;[x;z]]" by simp
qed


lemma lie_subalgebra:
  assumes h: "𝔥𝔤" "m1.subspace 𝔥" and closed: "x y. x  𝔥  y  𝔥  lie_bracket x y  𝔥"
  shows "lie_algebra 𝔥 scale lie_bracket"
proof -
  interpret 𝔥: vector_space_on 𝔥 scale
    apply unfold_locales
    apply (meson h(1) m1.scale_right_distrib_on subset_iff)
    apply (meson h(1) in_mono m1.scale_left_distrib_on)
    using h(1) m1.scale_scale_on m1.scale_one_on apply auto[2]
    by (simp_all add: h m1.subspace_add m1.subspace_0 m1.subspace_scale)

  show ?thesis
    apply (intro 𝔥.lie_algebraI)
    using alternating h(1) jacobi linearL' linearR' by (auto simp: closed subset_iff)
qed

end


subsection ‹Division algebras›

abbreviation (in algebra_on) "is_left_divisor x a b    x  S    a = amult x b"
abbreviation (in algebra_on) "is_right_divisor x a b    x  S    a = amult b x"

locale div_algebra_on = algebra_on +
  fixes divL::"'a'a'a" (* (infix "/L" 74) *)
    and divR::"'a'a'a" (* (infix "/R" 74) *)
  assumes divL: "aS; bS; b0  is_left_divisor (divL a b) a b"
      "aS; bS; b0  is_left_divisor y a b  y = (divL a b)"
    and divR: "aS; bS; b0  is_right_divisor (divR a b) a b"
      "aS; bS; b0  is_right_divisor y a b  y = (divR a b)"
begin
text ‹ In terms of the vocabulary of division rings,
  the expression terma = (divL a b)  b means that termdivL a b is a left divisor of terma,
  and conversely that terma is a right multiple of termdivL a b.›
text ‹
  For termb=0, the divisiors still exist as members of the correct type (necessarily),
  but they have no properties. Similarly for correctly-typed input outside the algebra.›

  lemma [simp]:
    assumes "aS" "bS" "b0"
    shows divL': "divL a b  S" "(divL a b)  b = a" "yS. a = y  b  y = divL a b"
      and divR': "divR a b  S" "b  (divR a b) = a" "yS. a = b  y  y = divR a b"
    using assms divL divR by simp_all
end

lemma (in algebra_on) div_algebra_onI:
  assumes "aS. bS. b0  (∃!xS. a=bx)  (∃!yS. a=yb)"
  shows "div_algebra_on S scale amult (λa b. THE y. yS  a=yb) (λa b. THE x. xS  a=bx)"
proof (unfold div_algebra_on_def div_algebra_on_axioms_def, intro conjI allI impI)
  fix a b x
  assume "aS" "bS" "b0"
  have exL: "∃!xS. a=xb" by (simp add: a  S b  S b  0 assms)
  from theI'[OF this]
    show L: "(THE y. y  S  a = y  b)  S" "a = (THE y. y  S  a = y  b)  b"
    by simp+
  have exR: "∃!xS. a=bx" by (simp add: a  S b  S b  0 assms)
  from theI'[OF this]
    show R: "(THE x. x  S  a = b  x)  S" "a = b  (THE x. x  S  a = b  x)"
    by simp+
  { assume "x  S  a = x  b"
    thus "x = (THE y. y  S  a = y  b)" using L exL by auto
  } { assume "x  S  a = b  x"
    thus "x = (THE x. x  S  a = b  x)" using R exR by auto
  }
qed (simp add: algebra_on_axioms)

lemma (in assoc_algebra_1_on) div_algebra_onI':
  fixes ainv adivL adivR
  defines "ainv a  (THE x. xS  a_id=xa  a_id=ax)"
    and "adivL b a  b  (ainv a)"
    and "adivR b a  (ainv a)  b"
  assumes "aS. a0  (xS. a_id=xa  a_id=ax)"
  shows "div_algebra_on S scale amult adivL adivR"
proof (unfold_locales)
  fix a b
  assume asm: "a  S" "b  S" "b  0"
  have inv_ex: "∃!xS. a_id=xb  a_id=bx"
    using assms(4) inverse_unique' asm(2,3) by metis
  let ?a = "THE x. x  S  a_id = x  b  a_id = b  x"
  from theI'[OF inv_ex] show 1: "adivR a b  S  a = b  adivR a b"
    unfolding adivR_def ainv_def apply (intro conjI)
    using asm(1) apply simp
    using amult_assoc amult_id(2) asm(1,2) is_ring_1_axioms(2) by (metis (no_types, lifting))
  from theI'[OF inv_ex] show 2: "adivL a b  S  a = adivL a b  b"
    unfolding adivL_def ainv_def apply (intro conjI)
    apply (simp add: asm(1))
    using amult_assoc asm(1,2) is_ring_1_axioms(3) by presburger
  { fix y assume "y  S  a = y  b"
    thus "y = adivL a b"
      by (metis inv_ex 2 amult_assoc asm(2) amult_id(2))
  } { fix y assume "y  S  a = b  y"
    thus "y = adivR a b"
    by (metis 1 amult_assoc asm(2) inv_ex is_ring_1_axioms(2)) }
qed

lemma (in assoc_algebra_on) div_algebra_on_imp_inverse:
  assumes "div_algebra_on S scale amult divL divR" "card S  2  infinite S"
  shows "a_idS. (aS. aa_id=a  a_ida=a)  (aS. a0  divL a_id a = divR a_id a)"
proof -
  obtain x where "x0" "xS"
    using assms(2) unfolding numeral_2_eq_2
    by (metis card_1_singleton_iff card_gt_0_iff card_le_Suc0_iff_eq insertI1 not_less_eq_eq
      rev_finite_subset subsetI zero_less_Suc)
  let ?id = "divL x x"
  show ?thesis
  proof (intro bexI conjI ballI impI)
    show 1: "?id  S"
      using assms unfolding div_algebra_on_def div_algebra_on_axioms_def
      using x  S x  0 by blast
    fix a assume "aS"
    show 2: "a  ?id = a"
      by (smt (verit) 1 aS xS x0 amult_assoc amult_closed assms(1) div_algebra_on.divL)
    show 3: "?id  a = a"
      by (smt (verit) aS xS x0 amult_assoc assms(1) div_algebra_on.divL(1) div_algebra_on.divR')
    assume "a0"
    show 4: "divL ?id a = divR ?id a"
      by (smt (verit) 1 3 aS a0 amult_assoc amult_closed assms(1) div_algebra_on.divL div_algebra_on.divR(2))
  qed
qed

lemma (in assoc_algebra_on) assoc_div_algebra_on_iff:
  assumes "card S  2  infinite S"
  shows "(divL divR. div_algebra_on S scale amult divL divR) 
      (id. unital_algebra_on S scale amult id  (aS. a0  (xS. ax=id  xa=id)))"
  proof (intro iffI)
    assume "id. unital_algebra_on S (*S) (⦁) id  (aS. a  0  (xS. a  x = id  x  a = id))"
    then obtain id
      where id: "idS" "aS. aid=a  ida=a" and inv: "aS. a0  (xS. ax=id  xa=id)"
      using unital_algebra_on.amult_id by blast
    then have unital: "unital_algebra_on S scale amult id"
      by (unfold_locales, simp_all)
    then have assoc_alg: "assoc_algebra_1_on S scale amult id"
      unfolding assoc_algebra_1_on_def assoc_algebra_1_on_axioms_def
      using assms unital_algebra_on.id_neq_0_if(2,3) assoc_algebra_on_axioms
      by blast
    show "divL divR. div_algebra_on S (*S) (⦁) divL divR"
      using assoc_algebra_1_on.div_algebra_onI'[OF assoc_alg] inv by fastforce
  next
    assume "divL divR. div_algebra_on S (*S) (⦁) divL divR"
    then obtain divL divR where div_alg: "div_algebra_on S (*S) (⦁) divL divR" by blast
    show "id. unital_algebra_on S (*S) (⦁) id  (aS. a  0  (xS. a  x = id  x  a = id))"
      using div_algebra_on_imp_inverse[OF div_alg assms] unital_algebra_on_axioms.intro assoc_algebra_on_axioms
      unfolding unital_algebra_on_def unital_algebra_on_axioms_def assoc_algebra_on_def
      by (smt (verit) div_alg div_algebra_on.divL(1) div_algebra_on.divR(1))
qed


locale assoc_div_algebra_on =
  assoc_algebra_1_on S scale amult a_id +
  div_algebra_on S scale amult "λa b. amult a (a_inv b)" "λa b. amult (a_inv b) a"
  for S
    and scale :: "'a::field  'b::ab_group_add  'b" (infixr *S 75)
    and amult :: "'b'b'b" (infixr  74)
    and a_id  :: 'b(𝟭)
    and a_inv :: "'b'b" (* (‹_› 73) *)
begin
text ‹
  The definition localeassoc_div_algebra_on is justified by @{thm assoc_div_algebra_on_iff} above:
  If we have an associative algebra already, the only way it can be a division algebra
  is to be unital as well. Since now left and right divisors can be defined through
  multiplicative inverses, we take only the inverse as a locale parameter, and construct
  the divisors.
  The only case we miss here (due to the requirement terma_id0) is the trivial algebra,
  which contains only the zero element (which acts as identity as well). This is for compatibility
  with the standard Isabelle/HOL type classes, which are subclasses of classzero_neq_one.
›

  abbreviation (input) divL :: "'b'b'b"
    where "divL a b  amult a (a_inv b)"

  abbreviation (input) divR :: "'b'b'b"
    where "divR a b  amult (a_inv b) a"

  lemma div_self_eq_id:
    assumes "aS" "a0"
    shows "divL a a = a_id"
      and "divR a a = a_id"
    apply (metis amult_id(1,3) assms divL'(3))
    by (metis amult_id(1,2) assms divR'(3))

end


locale finite_dimensional_assoc_div_algebra_on =
  assoc_div_algebra_on S scale amult a_id a_inv +
  finite_dimensional_vector_space_on S scale basis
  for S :: 'b::ab_group_add set
    and scale :: 'a::field  'b  'b  (infixr *S 75)
    and amult :: 'b'b'b             (infixr  74)
    and a_id  :: 'b                   (𝟭)
    and a_inv :: 'b'b                (*(‹_› 73)*)
    and basis :: 'b set


lemma (in assoc_div_algebra_on) finite_dimensional_assoc_div_algebra_onI [intro]:
  fixes basis :: "'b set"
  assumes finite_Basis: "finite basis"
    and independent_Basis: "¬ m1.dependent basis"
    and span_Basis: "m1.span basis = S"
    and basis_subset: "basis  S"
  shows "finite_dimensional_assoc_div_algebra_on S scale amult a_id a_inv basis"
  by (unfold_locales, simp_all add: assms)

end