Mathlib Map

Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Birational.partialIso

{X Y : AlgebraicGeometry.Scheme} → X.Birational Y → X.PartialIso Y

Choose a partial isomorphism witnessing that X and Y are birational.

Defined in
Mathlib.AlgebraicGeometry.Birational.Birational
Cited by
2 results in Mathlib
Foundations
Depth 3 from the axioms · uses Classical.choice
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

AlgebraicGeometry.Scheme.Birational.symm · cited by 0Birational.symmAlgebraicGeometry.Scheme.Birational.trans · cited by 0Birational.transAlgebraicGeometry.Scheme · cited by 2540AlgebraicGeometry.SchemeAlgebraicGeometry.Scheme.PartialIso · cited by 32Scheme.PartialIsoAlgebraicGeometry.Scheme.Birational · cited by 5Scheme.BirationalBirational.partialIsoCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.