Alex J Best comments

Results 47 comments of


                                            Alex J Best

feat(number_theory/geometry_of_numbers): Blichfeldt and Minkowski's theorems

@urkud indeed this still needs a lot of work, I'm slowly trying to make sure that the final theorem is actually usable for applications, and think more still needs doing....

feat: generalize_proofs tactic

There are still a couple of things to do to please the linters, but I'd be glad to receive feedback on this PR at this stage

Feature: "Add Explicit Type Annotation" code-action

+1 for having this as a code action in addition to a clickable

Better handling of SafetyErrors due to corrupted packages

@saraedum

feat(group_theory/iwasawa.lean): add a proof of the Iwasawa criterion for simplicity

Can you elaborate a bit @AntoineChambert-Loir ? The things you say are now formalized are they in this PR or somewhere else? I guess I see why knowing the normal...

feat(measure_theory/integral/lebesgue): add a lemma

Looks like this is broken as you removed `lintegral_add'` in another PR so I'm removing awaiting review for now

feat(algebra/module/polynomial): Modules over `R[X]`

I added a similar construction in #10944, it would be good to de-duplicate that material, and write that proof in terms of your new construction I think

Implement references / bibliography

Well doc-gen4 is written in lean, and the ideal situation IMO is that as much of the information is surfaced to Lean as possible so that we can do things...