How can we formulate Schanuel's conjecture in Lean?

Stream: maths

[Ingmar Velien]

How can we formulate Schanuel's conjecture in Lean?

[Eric Wieser]

For other readers; this was already somewhat discussed here: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Implementation.20of.20Schanuel's.20Conjecture.20in.20Lean.3F

[Scott Morrison]

I guess while we have docs#is_transcendence_basis, no one has defined transcendence_degree yet, so I'd be starting there.