Exterior algebras everywhere...

Stream: mathlib4

[Michael Stoll]

import Mathlib

lemma test (n : ℕ) (z : ℂ) :
    (1 - ‖z‖)⁻¹ * ((1 ^ (n + 1) - 0 ^ (n + 1)) / (↑n + 1)) = (1 - ‖z‖)⁻¹ / (↑n + 1) := by
  field_simp

#synth Zero ℕ -- ExteriorAlgebra.instZero ℕ

#minimize_imports
-- import Mathlib.Analysis.Complex.Basic
-- import Mathlib.LinearAlgebra.ExteriorAlgebra.Grading

Why do we need exterior algebras to know that the natural numbers have a zero?

[Eric Wieser]

docs#ExteriorAlgebra.instZero

[Yury G. Kudryashov]

Why do we have this instance and why is it in that file?

[Eric Wieser]

From the source:

-- Porting note: Lean needs to be reminded of this instance otherwise it cannot
-- synthesize 0 in the next theorem
instance (α : Type*) [MulZeroClass α] : Zero α := MulZeroClass.toZero

[Eric Wieser]

Yury G. Kudryashov said:

Why do we have this instance and why is it in that file?

Because during the port, review often didn't care about this kind of thing

[Yury G. Kudryashov]

I'll test whether we can delete it now.

[Eric Wieser]

Another answer would be "I don't know, you tell me!"; you're the author of #5459, though perhaps not the author of that line

[Yury G. Kudryashov]

@Xavier Roblot is the author of these lines.

[Yury G. Kudryashov]

I'm testing a fix with less side-effects (locally change the priority)

[Yury G. Kudryashov]

#9274

[Eric Wieser]

What goes wrong without that instance?

[Yury G. Kudryashov]

Elaboration timeout. I don't know why.

[Xavier Roblot]

Yury G. Kudryashov said:

Xavier Roblot is the author of these lines.

Indeed, although I do not remember all the details, it seemed a good idea at the time :sweat_smile:

[Michael Stoll]

import Mathlib.Analysis.Complex.Basic

#synth Zero ℕ -- LinearOrderedCommMonoidWithZero.toZero

which looks a bit more convincing.

What I find strange is that there seems to be no explicit Zero Nat instance. Replacing the import by Mathlib.Data.Nat.Basic gives "CommMonoidWithZero.toZero".

[Eric Wieser]

Part of the problem here is that all the Foo.toBar instances have the default priority, and also lean4#2905

[Michael Stoll]

I also often get "import Mathlib.RingTheory.DedekindDomain.Basic" as a suggestion from #minimize_imports when that is not actually necessary. I haven't tried to figure out where it is actually used, though.

[Michael Stoll]

import Mathlib

noncomputable
def logTaylor (n : ℕ) : ℂ → ℂ := fun z ↦ (Finset.range n).sum fun j ↦ (-1) ^ (j + 1) * z ^ j / j

lemma logTaylor_succ (n : ℕ) :
    logTaylor (n + 1) = logTaylor n + (fun z : ℂ ↦ (-1) ^ (n + 1) * z ^ n / n) := sorry

#minimize_imports
-- import Mathlib.Analysis.Complex.Basic

lemma logTaylor_at_zero (n : ℕ) : logTaylor n 0 = 0 := by
  induction n with
  | zero => sorry
  | succ n ih => simpa [logTaylor_succ, ih] using ne_or_eq n 0

#minimize_imports
-- import Mathlib.Analysis.Complex.Basic
-- import Mathlib.RingTheory.DedekindDomain.Basic

[Ruben Van de Velde]

import Mathlib

noncomputable
def logTaylor (n : ℕ) : ℂ → ℂ := fun z ↦ (Finset.range n).sum fun j ↦ (-1) ^ (j + 1) * z ^ j / j

lemma logTaylor_succ (n : ℕ) :
    logTaylor (n + 1) = logTaylor n + (fun z : ℂ ↦ (-1) ^ (n + 1) * z ^ n / n) := sorry

#minimize_imports
-- import Mathlib.Analysis.Complex.Basic

lemma logTaylor_at_zero (n : ℕ) : logTaylor n 0 = 0 := by
  induction n with
  | zero => sorry
  | succ n ih =>
    have := ne_or_eq n 0
    rw [logTaylor_succ, Pi.add_apply, ih, zero_add, div_eq_zero_iff]
    sorry

#minimize_imports

lemma logTaylor_at_zero' (n : ℕ) : logTaylor n 0 = 0 := by
  induction n with
  | zero => sorry
  | succ n ih =>
    have := ne_or_eq n 0
    rw [logTaylor_succ, Pi.add_apply, ih, zero_add, div_eq_zero_iff, mul_eq_zero]
    sorry

#minimize_imports
-- import Mathlib.Analysis.Complex.Basic
-- import Mathlib.RingTheory.DedekindDomain.Basic

[Ruben Van de Velde]

#synth NoZeroDivisors ℂ
@IsDomain.to_noZeroDivisors.{0} Complex Complex.instRingComplex
  (@IsDedekindDomain.toIsDomain.{0} Complex Complex.commRing
    (@IsPrincipalIdealRing.isDedekindDomain.{0} Complex Complex.commRing (@Field.isDomain.{0} Complex Complex.instField)
      (@EuclideanDomain.to_principal_ideal_domain.{0} Complex
        (@Field.toEuclideanDomain.{0} Complex Complex.instField))))

[Ruben Van de Velde]

import Mathlib

noncomputable
def logTaylor (n : ℕ) : ℂ → ℂ := fun z ↦ (Finset.range n).sum fun j ↦ (-1) ^ (j + 1) * z ^ j / j

lemma logTaylor_succ (n : ℕ) :
    logTaylor (n + 1) = logTaylor n + (fun z : ℂ ↦ (-1) ^ (n + 1) * z ^ n / n) := sorry

#minimize_imports
-- import Mathlib.Analysis.Complex.Basic

lemma logTaylor_at_zero (n : ℕ) : logTaylor n 0 = 0 := by
  induction n with
  | zero => sorry
  | succ n ih =>
    have := ne_or_eq n 0
    rw [logTaylor_succ, Pi.add_apply, ih, zero_add, div_eq_zero_iff]
    sorry

#minimize_imports

instance : IsDomain ℂ := Field.isDomain

lemma logTaylor_at_zero' (n : ℕ) : logTaylor n 0 = 0 := by
  induction n with
  | zero => sorry
  | succ n ih =>
    have := ne_or_eq n 0
    rw [logTaylor_succ, Pi.add_apply, ih, zero_add, div_eq_zero_iff, mul_eq_zero]
    sorry

#minimize_imports
-- import Mathlib.Analysis.Complex.Basic

[Eric Wieser]

Yeah, these weird dependencies are because extends on instances doesn't mean "set priority 100" in Lean 4

[Eric Wieser]

So the newer instance (ie, the one in a weird downstream file) always wins

[Eric Wieser]

Someone should make a patch to lean4 that restores the lean3 behavior, to see if it improves performance

[Yury G. Kudryashov]

^: the lean3 community edition behavior