Cardinality of permutation

Stream: Is there code for X?

[Teddy Baker]

I am trying to find the cardinality of a certain set, which is a basic problem in combinatorics. I want to find the number of maps Fin n → ℕ that have a given multiplicity for each element of the image. This is, of course, given by the multinomial coefficient Nat.multinomial s f, where s are the elements in the image, and f gives the multiplicity of these elements. I am having difficulty, however, establishing this correspondence. Here is a formalization of the problem which I believe is correct

import Mathlib

open Real
open Nat
open BigOperators

theorem fin_map_multinom
  (n : ℕ)
  (S : Finset (Fin n → ℕ))
  (f : Finsupp ℕ ℕ)
  (h₀ : Finsupp.sum f (fun _ => id) = n)
  (h₁ : ∀ s, s ∈ S ↔ ∀ j, f j = (Finset.filter (fun i => s i = j) Finset.univ).card) :
  S.card = Finsupp.multinomial f := by
  sorry

In the definition of multinomial coefficient, it says "The multinomial coefficient. Gives the number of strings consisting of symbols from s, where c ∈ s appears with multiplicity f c." However, the formal definition does not really appeal to that intuitive definition, and instead gives a formula. If I could find the equivalence between the formula and that intuitive definition, it would solve the problem.

In my investigation, I have looked through the various definitions of multinomial coefficients and related constructs, such as the multiset definition, compositions, and partitions, trying to find a theorem that expresses the cardinality in terms of the multinomial coefficient. Any such theorem would probably lead to a straightforward bijection that would close the goal. It seems that using induction and Finsupp.multinomial_update is probably the best idea I've come up with so far, but I think there should in principle be a more direct route, even though I haven't found it.

Thanks in advance for any help with this problem!

[Terence Tao]

I don't know if this is the shortest route, but one could show that the permutation group of Fin n acts transitively on S and the stabilizer is in bijection with the product of permutation groups and so has order Finsupp.prod f (fun j => Nat.factorial j), and then appeal to the orbit stabilizer theorem docs#MulAction.card_orbit_mul_card_stabilizer_eq_card_group

[Teddy Baker]

Thanks so much! I like the approach, it is very elegant and I can see how the proof would work. I've been working on implementing it, but I didn't manage to complete it due to a few technical difficulties. I'll be sure to share if I do end up completing the proof that way! Thanks again.

[Junyan Xu]

What you want is pretty close to the original proposed definition of multinomial:

lemma multinomial_eq {α} [fintype α] (f : α → ℕ) :
  multinomial f = nat.card {k : fin (∑ i, f i) → α // ∀ a, nat.card (k ⁻¹' {a}) = f a}

but we switched to the current (∑ i, f i)! / ∏ i, (f i)! midway because it's more convenient for the multinomial theorem.

I think @Antoine Chambert-Loir probably has some code about the first definition as he worked on counting permutations of given cycle type.

[Teddy Baker]

Thanks! That is good to know. I think it would probably be useful to have a lemma in Mathlib stating that that quantity is equal to the multinomial coefficient, even given the current definition. What do you think?

[Antoine Chambert-Loir]

Certainly.

[Antoine Chambert-Loir]

However, I don't think I have code that proves this result. What I proved (it should be PRed soon) is a proof of the formula for the number of permutations of given cycle type, and a group theoretic description of the centralizer of a permutation that implies this formula.
While the result you wish has a purely algebraic proof, it makes sense to provide (= I would love to see) a group-theoretic proof. Indeed, the numerator is the cardinality of the group Equiv.Perm (Fin (∑ i, f i)), which acts transitively on the indicated type, and the denominator is the cardinality of the stabilizer of a particular element.

[Teddy Baker]

Great, thanks, this has been a helpful discussion! In the meantime I think that I might do the proof by induction because it is a bit easier, but I'd like to see the group theoretic proof when it is completed!

[Terence Tao]

Here is half of the group theoretic proof, written in a way that does not explicitly refer to natural number labels. It's missing three claims that should all be straightforward, but I unfortunately don't have further time to devote to it, so anyone is welcome to pick it up from here.

import Mathlib

instance (α β : Type*) : MulAction (Equiv.Perm α) (α → β) where
  smul (φ: Equiv.Perm α) (f: α → β) := f ∘ (φ⁻¹ : Equiv.Perm α)
  one_smul _ := rfl
  mul_smul _ _ _ := rfl

open Classical BigOperators Nat

lemma Finsupp.multinomial_spec {β : Type*} [Fintype β] (f : β →₀ ℕ) : (∏ b, (f b)!) * Finsupp.multinomial f = (∑ b, f b)! := by
  rw [Finsupp.multinomial_eq]
  convert Nat.multinomial_spec f.support _ using 2
  . convert (Finset.prod_subset_one_on_sdiff _ _ _).symm
    . infer_instance
    . simp
    . intro x hx; simp at hx; simp [hx]
    simp
  convert (Finset.sum_subset_zero_on_sdiff _ _ _).symm
  . infer_instance
  . simp
  . intro x hx; simp at hx; exact hx
  simp

theorem fin_map_multinom
  {α : Type*} [Fintype α] {β: Type} [Fintype β] (f₀: α → β) :
  let m (b:β) := Fintype.card (f₀ ⁻¹' {b})
  Fintype.card { f: α → β | ∀ b : β, Fintype.card (f ⁻¹' {b}) = m b } = Finsupp.multinomial (Finsupp.equivFunOnFinite.symm m) := by
  set m := fun b ↦ Fintype.card (f₀ ⁻¹' {b})
  set S := { f: α → β | ∀ b : β, Fintype.card (f ⁻¹' {b}) = m b }
  change Fintype.card S = Finsupp.multinomial (Finsupp.equivFunOnFinite.symm m)

  have claim1 : S = MulAction.orbit (Equiv.Perm α) f₀ := by sorry
  have claim2 : Fintype.card (MulAction.stabilizer (Equiv.Perm α) f₀) = ∏ b : β, Fintype.card (Equiv.Perm (f₀ ⁻¹' {b})) := by sorry
  have claim3 : Fintype.card α = ∑ b, (Finsupp.equivFunOnFinite.symm m) b := by sorry

  have := MulAction.card_orbit_mul_card_stabilizer_eq_card_group (Equiv.Perm α) f₀
  simp_rw [<-claim1, claim2, Fintype.card_perm, claim3, <-Finsupp.multinomial_spec (Finsupp.equivFunOnFinite.symm m)] at this
  rw [mul_comm] at this
  change (∏ b, (m b)!) * Fintype.card S = (∏ b, (m b)!) * Finsupp.multinomial (Finsupp.equivFunOnFinite.symm m) at this
  rw [mul_eq_mul_left_iff] at this
  rcases this with this | this
  . assumption
  rw [Finset.prod_eq_zero_iff] at this
  rcases this with ⟨ b, hb, this ⟩
  contrapose! this
  exact Nat.factorial_ne_zero _

[Junyan Xu]

Just want to share another relevant thread: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/permutations.20preserving.20a.20function/near/391930331
(which is basically claim2, I think)

[Yaël Dillies]

The first instance is already in mathlib but stated using docs#DomMulAct

[Teddy Baker]

Here is the first claim :

have claim1 : S = MulAction.orbit (Equiv.Perm α) f₀ := by
    apply Set.ext
    intro f
    constructor
    · intro hf
      rw [Set.mem_setOf] at hf
      have bij_left (b : β) := Fintype.equivFinOfCardEq (hf b)
      have bij_right (b : β) := Fintype.equivFinOfCardEq (by rfl : Fintype.card (f₀ ⁻¹' {b}) = m b)
      let bij_b (b : β) := Equiv.trans (bij_left b) ((bij_right b).symm)
      have := Equiv.ofFiberEquiv_map bij_b
      rw [MulAction.mem_orbit_iff]
      use (Equiv.ofFiberEquiv bij_b)⁻¹
      funext a
      show f₀ ((Equiv.ofFiberEquiv bij_b) a) = f a
      rw [this a]
    · intro hf
      rw [MulAction.mem_orbit_iff] at hf
      rcases hf with ⟨ x, hx ⟩
      rw [Set.mem_setOf]
      intro b
      replace hx (a : α) : f₀ (x⁻¹ a) = f a := by rw [← hx]; exact rfl
      have subtype_equiv := @Equiv.subtypeEquivOfSubtype α α (fun a => f₀ a = b) x⁻¹
      have (g : α → β) : { a // g a = b } = g ⁻¹' {b} := by congr
      simp only [this _, hx] at subtype_equiv
      replace subtype_equiv := Fintype.card_congr subtype_equiv
      exact subtype_equiv

[Terence Tao]

And here is the third claim:

  have claim3 : Fintype.card α = ∑ b, (Finsupp.equivFunOnFinite.symm m) b := by
    change Fintype.card α = ∑ b, Fintype.card (f₀ ⁻¹' {b})
    convert Finset.card_eq_sum_card_fiberwise (f := f₀) (s := Finset.univ) (t := Finset.univ) (by simp) with b _
    convert (Set.toFinset_card _).symm
    ext x
    simp

It occurs to me that it might be slightly more efficient to refactor the proof using Multiset and in particular take advantage of the Multiset.map API. (This may also allow one to drop the Fintype β hypothesis, which is inessential.) But I guess one should get a complete working proof first and then worry about refactoring later.

[Terence Tao]

Yaël Dillies said:

The first instance is already in mathlib but stated using docs#DomMulAct

After following @Junyan Xu's link I see that the action is also stated explicitly in MulAction form as (a special case of) docs#arrowAction (maybe one should update the docs so that these two items mention each other?).

[Yaël Dillies]

Curious... We should only have one of these (and probably it's DomMulAct). @Eric Wieser, do you know what happened there?

[Junyan Xu]

docs#DomMulAct is basically docs#MulOpposite and it applies more generally for monoid actions, while docs#arrowAction uses the group inverse (which is an isomorphism between a group and its opposite). A docstring explaining the difference is certainly welcome! It's probably more convenient to use arrowAction in this case (and a proof using it was already there).

[Terence Tao]

By the way, I managed to piece together all the different components into a full proof (though there was some dependent type weirdness in the proof of claim2 that I don't really understand but I got it to work anyways - somehow convert can power through discrepancies in definitional equality for dependent types that rw, apply, or change cannot).

import Mathlib

open Classical BigOperators Nat MulAction Equiv

instance (α β : Type*) : MulAction (Perm α) (α → β) := arrowAction

variable {α β: Type*}

lemma arrowAction.mem_stabilizer_iff {f: α → β} {g : Perm α} :
    g ∈ stabilizer (Perm α) f ↔ f ∘ g = f := by rw [eq_comm, ← g.comp_symm_eq]; rfl

def φ_invFun {f: α → β} (g : ∀ b, Perm {a | f a = b}) (a : α) : α := g (f a) ⟨a, rfl⟩

lemma φ_invFun_eq {f: α → β} (g : ∀ b, Perm {a | f a = b}) {a : α} {b : β} (h : f a = b) :
    φ_invFun g a = g b ⟨a, h⟩ := by subst h; rfl

lemma comp_φ_invFun {f: α → β} (g : ∀ b, Perm {a | f a = b}) (a : α) : f (φ_invFun g a) = f a :=
  (g (f a) ⟨a, rfl⟩).prop

def φ_invFun_equiv {f: α → β} (g : ∀ b, Perm {a | f a = b}) : Perm α where
  toFun := φ_invFun g
  invFun := φ_invFun (fun b ↦ (g b).symm)
  left_inv a := by
    rw [φ_invFun_eq _ (comp_φ_invFun g a)]
    exact congr_arg Subtype.val ((g <| f a).left_inv _)
  right_inv a := by
    rw [φ_invFun_eq _ (comp_φ_invFun _ a)]
    exact congr_arg Subtype.val ((g <| f a).right_inv _)

def Φ {f: α → β} : stabilizer (Perm α) f ≃* (∀ b, Perm {a | f a = b}) where
  toFun g i := Perm.subtypePerm g fun a ↦ by
    simp only [Set.mem_setOf_eq]
    rw [← Function.comp_apply (f := f), arrowAction.mem_stabilizer_iff.mp g.prop]
  invFun g := ⟨φ_invFun_equiv g, by
    ext a; exact comp_φ_invFun (fun i ↦ (g i).symm) a⟩
  left_inv g := rfl
  right_inv g := by ext i a; apply φ_invFun_eq
  map_mul' g h := rfl

lemma Finsupp.multinomial_spec {β : Type*} [Fintype β] (f : β →₀ ℕ) : (∏ b, (f b)!) * Finsupp.multinomial f = (∑ b, f b)! := by
  rw [Finsupp.multinomial_eq]
  convert Nat.multinomial_spec f.support _ using 2
  . convert (Finset.prod_subset_one_on_sdiff _ _ _).symm
    . infer_instance
    . simp
    . intro x hx; simp at hx; simp [hx]
    simp
  convert (Finset.sum_subset_zero_on_sdiff _ _ _).symm
  . infer_instance
  . simp
  . intro x hx; simp at hx; exact hx
  simp

theorem fin_map_multinom
  {α : Type u_1} [Fintype α] {β: Type u_2} [Fintype β] (f₀: α → β) :
  let m (b:β) := Fintype.card (f₀ ⁻¹' {b})
  Fintype.card { f: α → β | ∀ b : β, Fintype.card (f ⁻¹' {b}) = m b } = Finsupp.multinomial (Finsupp.equivFunOnFinite.symm m) := by
  set m := fun b ↦ Fintype.card (f₀ ⁻¹' {b})
  set S := { f: α → β | ∀ b : β, Fintype.card (f ⁻¹' {b}) = m b }
  change Fintype.card S = Finsupp.multinomial (Finsupp.equivFunOnFinite.symm m)

  have claim1 : S = MulAction.orbit (Equiv.Perm α) f₀ := by
    apply Set.ext
    intro f
    constructor
    · intro hf
      rw [Set.mem_setOf] at hf
      have bij_left (b : β) := Fintype.equivFinOfCardEq (hf b)
      have bij_right (b : β) := Fintype.equivFinOfCardEq (by rfl : Fintype.card (f₀ ⁻¹' {b}) = m b)
      let bij_b (b : β) := Equiv.trans (bij_left b) ((bij_right b).symm)
      have := ofFiberEquiv_map bij_b
      rw [mem_orbit_iff]
      use (ofFiberEquiv bij_b)⁻¹
      funext a
      show f₀ ((ofFiberEquiv bij_b) a) = f a
      rw [this a]
    · intro hf
      rw [mem_orbit_iff] at hf
      rcases hf with ⟨ x, hx ⟩
      rw [Set.mem_setOf]
      intro b
      replace hx (a : α) : f₀ (x⁻¹ a) = f a := by rw [← hx]; exact rfl
      have subtype_equiv := @subtypeEquivOfSubtype α α (fun a => f₀ a = b) x⁻¹
      have (g : α → β) : { a // g a = b } = g ⁻¹' {b} := by congr
      simp only [this _, hx] at subtype_equiv
      replace subtype_equiv := Fintype.card_congr subtype_equiv
      exact subtype_equiv

  have claim2 : Fintype.card (stabilizer (Perm α) f₀) = ∏ b : β, Fintype.card (Perm (f₀ ⁻¹' {b})) := by
    rw [<- Fintype.ofEquiv_card Φ.toEquiv]
    set P : β → Type u_1 := fun b ↦ Perm (f₀ ⁻¹' {b})
    suffices : Fintype.card ((b:β) → P b) = ∏ b : β, Fintype.card (P b)
    . convert this -- convert is needed here to deal with two slightly different Fintype instances
    exact Fintype.card_pi

  have claim3 : Fintype.card α = ∑ b, (Finsupp.equivFunOnFinite.symm m) b := by
    change Fintype.card α = ∑ b, Fintype.card (f₀ ⁻¹' {b})
    convert Finset.card_eq_sum_card_fiberwise (f := f₀) (s := Finset.univ) (t := Finset.univ) (by simp) with b _
    convert (Set.toFinset_card _).symm
    ext x
    simp


  have := card_orbit_mul_card_stabilizer_eq_card_group (Perm α) f₀
  simp_rw [<-claim1, claim2, Fintype.card_perm, claim3, <-Finsupp.multinomial_spec (Finsupp.equivFunOnFinite.symm m)] at this
  rw [mul_comm] at this
  change (∏ b, (m b)!) * Fintype.card S = (∏ b, (m b)!) * Finsupp.multinomial (Finsupp.equivFunOnFinite.symm m) at this
  rw [mul_eq_mul_left_iff] at this
  apply or_iff_not_imp_right.mp this
  rw [<-ne_eq, Finset.prod_ne_zero_iff]
  intro b _
  exact factorial_ne_zero (m b)

[Eric Rodriguez]

convert is needed in that case because there is what is called a "diamond" of fintype instances, that is, the theorems you wanted to use are of the form @Fintype.card _ inst1 ... = _, but you wanted to have @Fintype.card _ inst2 ... = _, where inst1 and inst2 are two different instances of Fintype for the type you wanted. So these are not "exactly" the same theorems, but Fintype is a subsingleton; convert is aware of this, and will use the fact that inst1 and inst2 are equal to prove the goal. (You can probably see this by using show_term convert ...). There's also a second issue there, when you say have (b:β) : Fintype (P b) := by infer_instance; have forgets the term that you provide, so Fintype.card_pi again runs into the same issue. You should either be able to delete this line, or at worst replace it with let : Fintype (P b) := by infer_instance.

[Terence Tao]

Thanks! You were right, after deleting the infer_instance line, exact works just fine, and I have updated the code block accordingly. On the other hand, after inserting show_term, I see that the convert this line is hiding an enormous mess of motive manipulation that I am really glad I did not need to work out manually...

[Ruben Van de Velde]

So are we putting this in mathlib? :)

[Terence Tao]

It could do with a little refactoring and golfing. For instance if one refactors to work with Multiset instead of Finsupp then claim3 collapses to basically Multiset.card_map. And claim1 becomes a statement that is perhaps of its own interest: if f f₀: α → β then one has f = f₀ ∘ g for some g : Perm α if and only if Multiset.map f Finset.univ.val = Multiset.map f₀ Finset.univ.val.

[Eric Wieser]

Yaël Dillies said:

Curious... We should only have one of these (and probably it's DomMulAct). Eric Wieser, do you know what happened there?

Perhaps we are missing a type synonym that exchanges right and left actions by using the inverse element of a group? This is going to be a mess with the new notation though

[Eric Wieser]

And even DomMulAct is a flawed design that faces diamonds, but it at least contains them so only its users experience them

[Yury G. Kudryashov]

What are the diamonds for DomMulAct? It is rarely used at the moment, so it's not too late to fix it.

[Eric Wieser]

image.png

[Eric Wieser]

image.png

[Eric Wieser]

(this is from an extended version of "scalar actions in Lean's mathlib", which has turned into a thesis section. Rest assured I credit you for DomMulAct, and I have positive remarks about it too!)

[Yury G. Kudryashov]

Thank you!

[Yury G. Kudryashov]

Another solution would be to support non-instance actions and have notations like in your text for them.

[Eric Wieser]

I think lean 4 makes that pretty unviable, since SMul lemmas will refuse to apply to a non-instance action in the goal (finding instances by unification is no longer allowed)

[Eric Wieser]

Another way out would be SMul tag R M where tag : Unit is one of a handful of irreducible definitions such as leftMul or codAction leftMul

[Terence Tao]

Wow, it's rough being a left-handed Lean type in a universe made for right-handed types. Is there at least some sort of infer_instance? diagnostic tool that can help detect these diamonds? I just lost more than an hour to an (unrelated) silent diamond that was causing very weird heartbeat errors to pop up on extremely innocuous tactics (including stop!) until I finally caught it by chance when trying to narrow down a unification problem with congr. Having a tool to test for such instance diamonds would be nice.

[Eric Wieser]

What was the diamond in question that you ran into?

[Eric Wieser]

Right now our diagnostic tool is "post on Zulip", though indeed an automated solution would be superior!

[Eric Wieser]

(Once you've guessed where the diamond is, it's easy enough to verify that it's problematic)

[Yury G. Kudryashov]

By "support non-instance actions" I meant "set up theory so that it takes {_ : SMul M α}, not [SMul M α], like we do for σ-algebras in measure theory". But this will have unwanted side effects too.

[Terence Tao]

Eric Wieser said:

What was the diamond in question that you ran into?

It was one of my own creation. I had a commutative group G with discrete measurable structure on it, and a subgroup N of that group . I needed the discrete measurable structure on the quotient group G ⧸ N, so I made an instance for it: have _ : Measurable G ⧸ N = ⊤. However, I didn't realize that the quotient group already inherited a measurable structure from G, nevertheless the code was working okay despite the two instances except that random lines of code would time out using up a functionally infinite number of heartbeats (but if I commented out some other lines of code, then those random lines would compile, only for some other subsequent random line to fail). Eventually I isolated the problem with congr reducing to showing that the two instances were equal, and deleting my own instance (and replacing it with a proof that the pre-existing measurable structure on G ⧸ N was discrete) fixed everything. But it was a frustrating bug to hunt down, as (apart from the small example in the permutation code) I had not encountered this issue before, and nothing in the infoview or my diagnostic toolkit (except, ultimately, congr to try to understand why various defeq checks were sometimes (but not always!) taking near-infinite amounts of time) offered any clues (and the fact that errors only popped up after the code reached a certain length prevented me from isolating a MWE). (In particular, some sort of linter that was able to detect potentially problematic multiple instances assigned to the same object would help, though I don't know whether it is possible to do this without creating a lot of either false positives or false negatives.)

[Terence Tao]

Yury G. Kudryashov said:

By "support non-instance actions" I meant "set up theory so that it takes {_ : SMul M α}, not [SMul M α], like we do for σ-algebras in measure theory". But this will have unwanted side effects too.

Perhaps one could set up a small amount of support for a SMulRight structure, and then some tools to convert a SMulRight structure to a SMul structure and conversely, adding local instances manually as needed? Not sure if this is enough of a roadblock to cut off unwanted diamonds, though.

[Eric Wieser]

Unfortunately Right doesn't contain nearly enough information to specify which of many right actions you might want. I have a few paragraphs on this too; I'll upload the relevant thesis section here as a PDF when I'm back at my laptop next week.

[Terence Tao]

Oh I see. I imagine a similar problem will eventually come up if one wants to manipulate the high rank tensors that show up in Riemannian geometry, where there are multiple useful ways to contract indices that can't be inferred just from the type of the inputs.

[Terence Tao]

(I imagine Lean will barf heavily at trying to implement Penrose graphical notation, for instance.)

[Eric Wieser]

That notation would make a very cool formalization/widget project :)

[Antoine Chambert-Loir]

Since it is used here and I have to use it in another PR, I just made a PR out of claim2 : #9342

[Antoine Chambert-Loir]

Eric Wieser said:

[Example of a diamond caused by DomMulAct]
image.png

I don't understand the path on the right, using docs#Pi.instSMul : Why doesDomMulAct (G) act on G ? Just because, as types, DomMulAct (G) = G ?
(On the other hand, a similar diamond would also appear using f : G -> G -> DomMulAct(G).)

[Yury G. Kudryashov]

It acts on G → G using "domain" action.

[Antoine Chambert-Loir]

But precisely, mathematically speaking, there is no action of DomMulAct (G) on G (the domain of G -> G), hence my question.

[Eric Wieser]

Pi.instSmul is being instantiated with G -> G as the codomain, not G

[Eric Wieser]

Perhaps I need to show the arguments in the diagram too, but then I start to have space issues

[Antoine Chambert-Loir]

Didn't you switch the two labels on the red path?

[Antoine Chambert-Loir]

(I don't know, I'm lost…)

[Eric Wieser]

I think the labels are correct, but perhaps this presentation is non-optimal

[Eric Wieser]

The top arrow is saying that the smul that it originates from is unfolded to the expression it points to, using the instance specified

[Antoine Chambert-Loir]

OK, I think I understand.
Mathematically speaking, DomMulAct(G) acts on G -> H by acting on the source, but if DomMulAct(G) acts on H, it also acts on G -> H by acting on the target.
Consequently, DomMulAct(G) acts on G -> (G -> G) in two different ways : the first one is the action on the source, and the second one is the action on the target, and these actions are distinct.

A similar problem would consider DomMulAct (G) acting on G → DomMulAct (G) : for f : G → DomMulAct(G) and g : DomMulAct (G), one has (g • f) (a) = f (g⁻¹ a) ≠ g • f(a) = f(a) g⁻¹.

[Eric Wieser]

DomMulAct has no inverses, but otherwise that example is correct

[Antoine Chambert-Loir]

Apparently, I confused docs#DomMulAct and docs#arrowAction…

[Antoine Chambert-Loir]

The correct line would thus be : (g • f) (a) = f (a * g) ≠ g • f(a) = f(a) * g.

[Eric Wieser]

Modulo the missing functions to transfer across the identification, yes

[Antoine Chambert-Loir]

One day or another, we shall need to teach Lean to cope with such ambiguities.

[Eric Wieser]

Eric Wieser said:

I have a few paragraphs on this too; I'll upload the relevant thesis section here as a PDF when I'm back at my laptop next week.

efw-scalars-2024-01-04.pdf

Eric Wieser said:

Another way out would be SMul tag R M where tag : Unit is one of a handful of irreducible definitions such as leftMul or codAction leftMul

There is now a short outline of this approach too.