Eigenproperties of symmetric matrices

Stream: new members

[Gabriel Moise]

Hello! I have been working towards a file that contains properties of symmetric matrices with real coefficients, like the fact that all their eigenvalues are real and each has a corresponding real eigenvector, as I did not see them in the documentation on linear algebra. The thing is that I am not an experienced Lean programmer, and although I tried to make the code as clear as possible and with minimal repeated work, I am not sure that the code is PR-worthy. Another thing is that the whole file is 400-lines and it has a substantial amount of helping lemmas, so it would be hard to review, but I don't know if I can break it into smaller pieces, as statements follow from previous ones and so on. Should I have a "more experienced" opinion on what I wrote and maybe discuss its potential? :smile:

[Johan Commelin]

Sure, you can link to your code here. If some of those helper lemmas are really about something slightly more general, you can probably PR those to other files.

[Johan Commelin]

And then have a second PR about eigenvalues of symmetric matrices, and such

[Gabriel Moise]

https://github.com/gabrielmoise/Lean-work/blob/master/symm_matrix.lean
Yes, some of the lemmas are more general (delimitated them with comments) and would fit into the data.matrix.basic file

[Johan Commelin]

The stuff up to line 186 seems generic matrix stuff. So that would make a great first PR. You will have to scatter those lemmas into their natural places in the library, which means you'll be editing 2 or 3 files probably. You might discover some duplicates, I didn't look carefully for those though.

[Johan Commelin]

If you are not scared of getting 50 constructive feedback comments on your PR, then I would say "go for it!"

[Kevin Buzzard]

Thank you for the module docstring! There is quite a precise format which we ask is followed, and which your docstring doesn't quite match yet: it's here.

[Eric Wieser]

I see a number of lemmas there that are hiding in the library already (eg vec_eq_unfold' is docs#funext_iff), but the code certainly looks ready-for-mathlib-review even if not ready-for-mathlib-merge

[Eric Wieser]

vec_smul_zero should be covered by docs#pi.no_zero_smul_divisors but perhaps that doesn't exist yet.... You should be able to replace it with docs#smul_eq_zero

[Gabriel Moise]

What do you mean by ready-for-mathlib-review? That I should PR it? Btw thanks already for the feedback, it helps a lot :smile:

[Eric Wieser]

I meant to backup what @Johan Commelin said about going for a PR if not afraid of 50 or so comments

[Kevin Buzzard]

Yes, please PR it :-) And if you don't change the module docstring beforehand then this will be my first comment :-)

[Gabriel Moise]

I am doing that right now, hopefully it will be up to the standard.

[Eric Wieser]

Another quick thing to address before PRing; take a quick look at #style

[Eric Wieser]

Oh. That link doesn't work

[Eric Wieser]

Well, what jumps out now is the lack of spaces inside {} and the multiple tactics on a single line

[Eric Wieser]

https://leanprover-community.github.io/contribute/style.html#tactic-mode

[Eric Wieser]

If you fix those part-way through PRing them github will start hiding comments

[Gabriel Moise]

And btw how can I make a PR to an already existing file from mathlib? I should mention that I have an outdated mention of mathlib.

[Eric Wieser]

You can create a branch that starts on the version of mathlib you were using

[Scott Morrison]

#style hopefully works now?

[Johan Commelin]

Eric Wieser said:

I meant to backup what Johan Commelin said about going for a PR if not afraid of 50 or so comments

@Gabriel Moise Note that those 50 comments are standard for everyone who makes a first PR. We all started that way :sweat_smile:

[Kevin Buzzard]

@Gabriel Moise to follow up what Eric was sayign abuot {} and lines, here's what your first lemma shoudl look like:

@[simp]
lemma vec_eq_unfold (x y : V → R) : (λ (i : V), x i) = (λ (i : V), y i) ↔ ∀ (i : V), x i = y i :=
begin
  split,
  { intros hyp i,
    exact congr_fun hyp i },
  { intro hyp,
    ext i;
    simp [hyp] }
end

[Gabriel Moise]

Oh I really want as many comments as possible.
Now I am following some guides on how to make the first PR as I am not very experienced with GitHub either.

[Kevin Buzzard]

If you do those fixes (e.g. simp[ -> simp [, repeat{ -> repeat { etc) before you PR then it will save a lot of noise during the PR process.

[Kevin Buzzard]

{intro -> { intro. Also you have a non-terminal simp on line 119 and another on line 145 ,148 etc.

[Gabriel Moise]

So the goal is to only use simp only when I want to close goals, and not throughout the proof as intermediate steps as well.

[Kevin Buzzard]

Right, but there are tricks, eg change simp to squeeze_simp to find out what it actually did, and then do it manually yourself

[Gabriel Moise]

Eric Wieser said:

I see a number of lemmas there that are hiding in the library already (eg vec_eq_unfold' is docs#funext_iff), but the code certainly looks ready-for-mathlib-review even if not ready-for-mathlib-merge

This link doesn't work for me.

[Johan Commelin]

docs#function.funext_iff

[Eric Wieser]

If you're looking for a tiny first PR to practice on, your mul_vec_smul_assoc lemma looks like one that mathlib is missing, and it would go in data/matrix/basic.lean (after addressing your could not turn ℂ into general R comment)

[Gabriel Moise]

Eric Wieser said:

If you're looking for a tiny first PR to practice on, your mul_vec_smul_assoc lemma looks like one that mathlib is missing, and it would go in data/matrix/basic.lean (after addressing your could not turn ℂ into general R comment)

Was working on PR-ing the vec_mul_mul_vec_assoc lemma, but thanks for the advice.

[Eric Wieser]

That one is probably easier anyway!

[Eric Wieser]

Although you can prove it much more succinctly!

(dot_product_assoc y M x).symm

[Gabriel Moise]

Eric Wieser said:

If you're looking for a tiny first PR to practice on, your mul_vec_smul_assoc lemma looks like one that mathlib is missing, and it would go in data/matrix/basic.lean (after addressing your could not turn ℂ into general R comment)

My problem with (could not turn C into general R) was that I needed to instantiate R with [comm_semigroup R] and then (since I already had [ring R]) some weird interactions happened. Trying to understand the root of the problem, I noticed that:

lemma test_mul_comm {α : Type*} [comm_semigroup α] (a b : α) : a * b = b * a :=
begin
  exact mul_comm a b,
end

lemma test_mul_comm2 {α : Type*} [comm_semigroup α] [ring α] (a b : α) : a * b = b * a :=
begin
  exact mul_comm a b, -- no longer works
end

and this is a little confusing to me.

[Kevin Buzzard]

comm_semigroup alpha means "put a commutative semigroup structure on alpha". And ring alpha then means "put a totally unrelated ring structure on alpha (but use the same symbol * for the multiplication)". This is surely not what you want. Do you want comm_ring alpha?

[Kevin Buzzard]

If you've proved theorems about rings and then want to prove some more theorems about commutative rings, you could use sections, and have variable assumptions in the sections, e.g.

variable (R : Type*)

section ring_stuff

variable [ring R]

<ringy theorems>

end ring_stuff

section comm_ring_stuff

variable [comm_ring R]

<comm_ringy theorems>

end comm_ring_stuff

[Kevin Buzzard]

Alternatively you could let all your rings be called R and all your comm_rings be called A. I tend to do this when I'm doing groups, with groups called G and abelian groups called A.

[Gabriel Moise]

Can't I include the comm_ring_stuff section in the ring_stuff section (nesting them) or is it a bad idea?

[Johan Commelin]

@Gabriel Moise If you have variables {R : Type*} [ring R] [comm_ring R] then you get two completely unrelated ring structures on R and Lean will get mightily confused.

[Johan Commelin]

So nesting will not work.

[Gabriel Moise]

Can I get permission to push a branch to mathlib, please? My username is gabrielmoise

[Johan Commelin]

Invitation sent: https://github.com/leanprover-community/mathlib/invitations

[Gabriel Moise]

Thanks a lot!

[Gabriel Moise]

Does the continuous integration / Build mathlib (push) part of the check of a PR generally take a lot?

[Eric Rodriguez]

yep ^^

[Bryan Gin-ge Chen]

It mostly depends on how deep the changes you've made are in the import graph. A modification to a leaf file will probably compile in a few seconds, but adding stuff to a basic algebra or order file will force a recompilation of almost all of mathlib.

[Patrick Massot]

I'm late to the party but I'm extremely worried about trying to merge this into mathlib. Why working with matrices instead of endomorphisms? I think going down the mathematical road (first endomorphisms and then deduce results about matrices if they are needed somewhere) would be much cleaner.

[Patrick Massot]

We already have things in https://leanprover-community.github.io/mathlib_docs/linear_algebra/eigenspace.html

[Eric Wieser]

Even with that being the case, I think doing this the matrix way will have filled a bunch of lemma gaps in the existing matrix API; we don't have to merge everything to extract value out of this effort

[Eric Wieser]

I agree that we should use the endomorphism definitions wherever possible though

[Johan Commelin]

I agree with what Patrick said. We definitely don't want to do a whole lot of work on matrices that is better done for endomorphisms first. But I also think that all the helper lemmas that you found are helping to fill out the matrix API.
So when those api gaps are filled, we should discuss here on zulip what is the best way to move forward with the symmetric stuff. It should tie in well with the rest of the library (e.g. the file that Patrick linked to).

[Hanting Zhang]

Eric Wieser said:

I agree that we should use the endomorphism definitions wherever possible though

I've always found this weird, but is there any particular reason why docs#linear_map.trace is defined using docs#matrix.trace? It could be defined in terms of the roots of the characteristic polynomial, right? I don't know about infinite dimensional stuff though.

[Kevin Buzzard]

And the characteristic polynomial of an endomorphism is presumably defined using the determinant of a matrix? I don't see how you can get away from matrices here.

[Hanting Zhang]

Oh, true.

[Hanting Zhang]

Wikipedia explains a coordinate-free definition of trace (https://en.wikipedia.org/wiki/Trace_(linear_algebra)#Coordinate-free_definition), so it seems like something can be done?

[Kevin Buzzard]

To write down the inverse map Hom(V,V) -> V tensor V^* (necessary to do the computation) you need to pick a basis. The map V tensor V^* -> Hom(V,V) is not a bijection in the infinite-dimensional case (it's an injection, with image the finite rank maps)

[Hanting Zhang]

:anguish: Ooh, thanks for clarifying! The assumption is still hidden in there

[Kevin Buzzard]

Writing maps from tensor products is easy because of the universal property. To write down a map into a tensor product is a different story; to access all elements of the tensor product you typically need a "model", i.e. a basis for each of the vector spaces, giving you a basis for the tensor product.

[Stepan Nesterov]

But there is a coordinate-free definition of determinant via top exterior powers. Then det(1+tA)=1+t*tr(A) in k[t]/(t^2) does the job, right?

[Kevin Buzzard]

Models of objects in mathematics are fascinating and I knew nothing about this stuff until I started formalising. The universal property only gets you so far. To prove that the kernel of the canonical map $R\to R[1/S]$ is the r such that there exists s with rs=0 you don't seem to be able to get this from the universal property alone: you seem to need the explicit model of R[1/S] as R x S / ~. Picking a model for the localisation is like picking a basis for the vector space.

[Johan Commelin]

I guess you can push everything into the computation that $\bigwedge^n V \cong k$ if $\dim(V) = n$. You will need to use a basis at some point.

[Kevin Buzzard]

Yes, in this approach the basis is hidden in the proof that the n'th wedge power is 1-dimensional.

[Kevin Buzzard]

Even talking about dimension is problematic if you're not allowed to pick a basis. Dimension is "size of any basis".

[Kevin Buzzard]

We need a constructivist to explain to us what's going on. I'll ask on Twitter.

[Stepan Nesterov]

We probably need bases at some point in development, but not matrices.
I was just making the point that there is a fancy definition which is independent of a basis by construction.

[Stepan Nesterov]

Kevin Buzzard said:

Even talking about dimension is problematic if you're not allowed to pick a basis. Dimension is "size of any basis".

Dimension is a size of a maximal flag of subspaces minus 1 ;)

[Johan Commelin]

Aha, and then you prove by induction that the top wedge is 1-dimensional. Sweet.

[Kevin Buzzard]

How do you know a maximal flag exists? Wait -- I don't even understand the question. What does it mean to say a vector space is finite-dimensional? Is the definition that it's Noetherian? In which case we might be on to something.

[Johan Commelin]

In mathlib finite_dimensional is in terms of noetherian, yes.

[Kevin Buzzard]

But how do we know that all max flags have the same size?

[Stepan Nesterov]

Kevin Buzzard said:

To write down the inverse map Hom(V,V) -> V tensor V^* (necessary to do the computation) you need to pick a basis. The map V tensor V^* -> Hom(V,V) is not a bijection in the infinite-dimensional case (it's an injection, with image the finite rank maps)

But we don't need to write it down, right? You can characterize the image of id uniquely as the only GL(V)-invariant vector such that the natural pairing V tensor V* sends it to 1.

[Stepan Nesterov]

But how do we prove it exists though

[Stepan Nesterov]

Developing even basics of representation theory of GL(V), which we do not know to be an algebraic group lacking (g \in GL(V) \iff det(g) \neq 0) seems challenging

[Kevin Buzzard]

challenging unless you pick a basis, which I thoroughly recommend doing :-)

[Stepan Nesterov]

Kevin Buzzard said:

But how do we know that all max flags have the same size?

Because GL(V) acts transitively on the set of all complete flags by induction

[Stepan Nesterov]

It suffices to prove that GL(V) acts transitively on vectors

[Stepan Nesterov]

Which you can reduce to the 2-dimensional case

[Kevin Buzzard]

I don't think we can induct. I think this is the problem. It's like trying to prove things on fintype by inducting, but not every fintype is equal to a disjoint union of two smaller fintypes.

[Kevin Buzzard]

I am still not convinced we can define dimension without picking a basis. For all I know in a Noetherian F-vector space there are flags of arbitrarily large finite length.

[Stepan Nesterov]

That's like Noetherian induction in algebraic geometry, yes

[Stepan Nesterov]

All proper subtypes ok => type ok

[Stepan Nesterov]

Maybe the right proof is to figure out exterior powers and than obtain invariance of dimension as a corollary?

[Stepan Nesterov]

When you define determinant by a formula, you don't use that all bases have the same size at all, you just define

[Kevin Buzzard]

I'm not sure how to do this in type theory. Coincidentally I was thinking about this today when formalising liquid stuff. We're supposed to be proving a theorem about fintypes by induction on size of the fintype but I realised that this was a bit terrifying because I would need to prove that the truth value of my statement about fintypes factored through the cardinality function.

[Adam Topaz]

Another characterization of f.d.v.s. is as the compact objects in the category of vector spaces

[Kevin Buzzard]

In the end I decided to switch to finsets.

[Kevin Buzzard]

Adam Topaz said:

Another characterization of f.d.v.s. is as the compact objects in the category of vector spaces

This still doesn't give you a well-defined dimension without picking a basis.

[Adam Topaz]

The dimension is the trace of the identity morphism

[Adam Topaz]

sorry I'm just catching up on this discussion now

[Stepan Nesterov]

Adam Topaz said:

The dimension is the trace of the identity morphism

does not work in char p :(

[Adam Topaz]

bah take Witt vectors

[Adam Topaz]

(obviously that's not a real suggestion, but I'm trying to come up with a basis-free definition like Kevin was asking)

[Stepan Nesterov]

What if we define finite-dimensional as V -> V** is surjective?

[Adam Topaz]

What's wrong with the compact object definition?

[Adam Topaz]

There's this notion of a compact closed monoidal category where objects have duals. If you have some general closed monoidal category which also happens to be locally presentable (and maybe one needs some compatibility with the monoidal structure) is it not the case that the subcategory of compact objects is compact closed monoidal? I couldn't find anything along these lines on the nLab, but I'm sure something along these lines has been written down somewhere...

[Adam Topaz]

Oh, and you can define the dimension of a vector space $V$ over $k$ as the Krull dimension of $\mathrm{Sym}_k^*V$ :smile:

[Adam Topaz]

(again, not a serious suggestion)

[Kevin Buzzard]

The problem with that definition is that a general Noetherian ring might have infinite Krull dimension.

[Adam Topaz]

Why is that a problem?

[Stepan Nesterov]

The following seems to be (an overcomplicated) strategy:
Step 1. If k is the field of real numbers, and V is a finite-dimensional vector space, then V is locally compact with respect to the weak topology defined by V*. Therefore, V has a unique Haar measure up to scaling. Define for an f: V -> V its determinant to be the constant, on which it multiplies the Haar measure if f is in the connected component of GL(V), and negative that constant otherwise. Define tr(f)=d/dt det(1+tf) at 0.
Step 2. If k is a field of complex numbers, then End_k(V) is a subspace of End_R(V). Define trace over k as half the trace over the reals.
Step 3. If k is a ring Z[x1,...,xn], embed it into C and use step 2.
Step 4. If k a ring of finite type over Z, use step 4, and then pass to colimits.

[Stepan Nesterov]

We don't even need to care about the sign of det, I guess

[Kevin Buzzard]

I would be happy with a construction over the reals and I can quite believe that you can then spread out. So my instinct is to look for the sneaky basis-choosing in step 1.

[Stepan Nesterov]

Ok, one issue is to prove V is Hausdorff aka that linear functions separate points of V.

[Kevin Buzzard]

Maybe it's hard to prove that V is locally compact? My model for a "bad" V is one which has linearly independent subsets of size n for all n but which is still Noetherian.

[Kevin Buzzard]

If we're defining V to be finite-dimensional if it's Noetherian then we need to rule out the possibility that there are Noetherian modules with arbitrary large ascending chains all of which are finite. This is what choosing the basis does for you -- you can show the basis is a concrete bound for the length of any chain. But a random Noetherian module can I think have arbitrarily large ascending chains -- there are infinite-dimensional Noetherian rings, right?

[Adam Topaz]

Yeah I think there are examples by Nagata?

[Stepan Nesterov]

Guess you can prove existence of linear functionals by just throwing in Zorn lemma and not caring.
If we know that V* is finitely generated, then you can get a closed embedding V -> R^n, hence V is locally compact. Not sure if that counts as picking a basis, more of a usage that V is a projective R-module.

[Stepan Nesterov]

The thing I'm not so sure about is why det(1+tf) is differentiable

[Stepan Nesterov]

Well, let's say that differentiability in V makes sense somehow and that we have an access to a smooth bump function \phi with integral 1. Then det(1+tf)= \int \phi(1+tf(x)) dx, which is smooth by some Analysis 2, I guess?

[Kevin Buzzard]

I think that when it has got to this point it's just better to ask a constructivist/foundational person to prove that it can't be done without picking a basis, rather than trying to construct more elaborate arguments. My mental model of mathematics says that if you can't do it with easy stuff then you're never going to be doing it with Haar measure.

[Stepan Nesterov]

Well, it does sometimes happen that an elaborate argument for a simple fact is actually non-circular. There is a proof of the fundamental theorem of algebra using Gauss-Bonnet theorem: https://arxiv.org/abs/1106.0924
There was also the proof using stochastic integration, I believe

[David Wärn]

The sensible constructive definition of "V is finite dimensional" is "V is merely isomorphic to $k^n$ for some $n$". In mathlib the type for this is trunc (Σ n : ℕ, V ≃ₗ[k] fin n → k). This is by definition a subsingleton but it still carries data. It's perfectly analogous to the definition of "A is a finite type", which is (equivalent to) "A merely bijects with fin n for some n" (even in Lean!).

So basically, as in real mathematics, if V is finite dimensional, then it has a basis, and you can use this basis in your constructions, provided that you then check that the choice of basis doesn't matter (this is part of trunc-elimination). For example if you want to define the dimension of a finite-dimensional vector space, you have to check that all bases have the same size. In other words, if $k^m \cong k^n$ then $m = n$. This is not totally obvious but it's something we learn how to do. Again this is perfectly analogous to the cardinality of a finite type -- you have to check that $[m] \cong [n]$ implies $m = n$.

Returning to the definition of trace, consider the fact that if V is finite-dimensional then the evaluation map $V \to V^{**}$ is an isomorphism. This is a subsingleton (a map has at most one two-sided inverse), so the second part of trunc-elimination is trivial and we can just assume $V$ has a finite basis. So it suffices to check it for $k^n$ basically, which is straightforward. Same thing with the fact that the obvious map $V \otimes V^* \to Hom_k(V, V)$ is an isomorphism when $V$ is finite-dimensional, or the fact that $\bigwedge^n V$ is one-dimensional for $n = \dim V$.

[David Wärn]

NB there are weaker definitions of "A is a finite set" for which the cardinality of A becomes noncomputable. For example knowing that A embeds in a finite set does not let you compute the cardinality of A -- any proposition embeds in unit, but computing the cardinality of a proposition means deciding if it's true or false. (Similarly knowing that A has a surjection from a finite set does not help.) By the same token, knowing that V embeds in a finite-dimensional vector space (or doesn't have an infinite independent set or whatever) doesn't let you compute the dimension of V.

[Kevin Buzzard]

I see, so the issue is that we have a nonconstructive definition of finite-dimensional ("V is Noetherian") and then we're trying to do something which moves from the Prop world ("there exists a basis") to the Type world ("this is its size" / "this is a matrix").

[Gabriel Moise]

Patrick Massot said:

I'm late to the party but I'm extremely worried about trying to merge this into mathlib. Why working with matrices instead of endomorphisms? I think going down the mathematical road (first endomorphisms and then deduce results about matrices if they are needed somewhere) would be much cleaner.

Thanks for the suggestion! I made that file to practice solving some lemmas for a uni project I have. Clearly, my approach is clumsy, but maybe some of the simple lemmas that I use could be added to mathlib to make calculations easier (so far I am trying to add simple lemmas to the data.matrix.basic file about dot_products and stuff like that).

[Gabriel Moise]

I do have a question though, do you think it would something desired to also add a section about vectors on C and operations with them? Like in my file I have a definition vec_conj and some lemmas with dot_product and norm_sq? Would those help mathlib and if so, where do they fit in?

[Johan Commelin]

With C you mean the complex numbers?

[Johan Commelin]

I think there is already a bunch of stuff for an "arbitrary" field that is is_R_or_C.

[Johan Commelin]

But I haven't used that much. Hopefully others can chime in.

[Gabriel Moise]

Yes, I meant the complex numbers.

[Gabriel Moise]

Oh, I will have a look into that then.

[Gabriel Moise]

But for that I think I would need to prove that (V -> C) is an instance of is_R_or_C, with V an indexing type.

[Johan Commelin]

No, that won't work. The coefficients of a vector live in such a field, but the vector itself doesn't.

[Eric Wieser]

Does it make sense to define a pi.star_ring which would provide vec_conj as docs#star?

[Eric Wieser]

We already imbue pi types with most operations elementwise

[Eric Wieser]

So doing the same for the star "operator" doesn't seem totally unreasonable

[Scott Morrison]

I like it.

[Eric Wieser]

I'll make the quick PR

[Eric Wieser]

#7342

[Gabriel Moise]

I noticed that having a coercion from real-valued matrices to complex-valued matrices means that I need to write a lot of explicit coercions(M : matrix V V ℂ), but that makes reading difficult especially when I have equations like in line 248 from https://github.com/gabrielmoise/Lean-work/blob/master/symm_matrix.lean :

have h₁ : mul_vec (M : matrix V V ℂ) (a • v + b • w) = mul_vec (M : matrix V V ℂ) (a • v) + mul_vec (M : matrix V V ℂ) (b • w),

and I would like to transform this thing into a notation. Can I create a notation that depends on an input M of a certain type (matrix V V ℝ)?

[Scott Morrison]

Sure --- just set up the notation, and it won't typecheck if you give it the wrong input. This is not something you really have to specify at the notation level.

[Eric Wieser]

Are you sure you need the coercions at all?

[Eric Wieser]

That is, can you state the lemmas for a more general case than \C which includes \R?

[Scott Morrison]

I commend is_R_or_C to you!

[Gabriel Moise]

Well, my proofs require the fact that I am using a matrix that is real-valued and my matrix-vector operations require that this matrix is coerced to a complex-valued operation. So that was my first idea, but I can adjust it. What I wanted to try for now is something like this: (don't mind the notation, it will probably be changed to something more appropriate)

variables {m n : Type*} [fintype m] [fintype n]
instance : has_coe (matrix m n ℝ) (matrix m n ℂ) := ⟨λ M, (λ i j, ⟨M i j, 0⟩)⟩

notation `$` := λ (M : matrix m n ℝ), (M : matrix m n ℂ) -- invalid notation declaration, contains reference to local variables

But apparently this doesn't work.

[Gabriel Moise]

Scott Morrison said:

I commend is_R_or_C to you!

I am exploring this idea as well, thank you! :smile:

[Gabriel Moise]

Gabriel Moise said:

https://github.com/gabrielmoise/Lean-work/blob/master/symm_matrix.lean
Yes, some of the lemmas are more general (delimitated them with comments) and would fit into the data.matrix.basic file

I updated the file so that now it is hopefully up to a better standard. I'll probably try to PR some lemmas from there. Thanks for the help! :smile: (any other suggestion is more than welcomed)

[Eric Wieser]

The star_test instance you have is provided for you if you import algebra.star.pi

[Gabriel Moise]

Oh thanks for the PR you did then! :smile:

[Eric Wieser]

Although from what I can tell you didn't end up using it anyway

[Gabriel Moise]

Yeah, I had two lemmas using the star instances, but I managed to avoid using them in the important theorems. But it was a good exercise.

[Eric Wieser]

I think there's some glue missing between is_R_or_C and has_star that might help eventually

[Gabriel Moise]

How can I specify that I am working on a ring structure that has (1 : R) ≠ 0 i.e. that this is not a zero ring?

lemma test [ring R] [specify (1 : R) ≠ 0] : ...

[Eric Wieser]

[nontrivial R]

[Eric Wieser]

Which gives you access to docs#zero_ne_one