Inverse element for surreal number

DOI10.2478/FORMA-2024-0005MaRDI QIDQ6966341zbMATH OpenFDO

Authors Karol Pąk

Publication date 30 June 2025

Published in Formalized Mathematics (Search for Journal in Brave)

Copyright license Creative Commons Attribution-ShareAlike 3.0 Unported

Full work available at URL https://doi.org/10.2478/FORMA-2024-0005

zbMATH Keywords

Conway's gamesurreal numbers

Mathematics Subject Classification ID

Nonstandard models in mathematics (03H05) Ordered fields (12J15) Formalization of mathematics in connection with theorem provers (68V20)

Cites work

• A Short Presentation of Coq
• An introduction to Conway's games and numbers
• Concrete semantics. With Isabelle/HOL
• Conway normal form: bridging approaches for comprehensive formalization of surreal numbers
• Conway numbers -- formal introduction
• scientific article; zbMATH DE number 3521878 (Why is no real title available?)
• scientific article; zbMATH DE number 1568491 (Why is no real title available?)
• Integration of game theoretic and tree theoretic approaches to Conway numbers
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Isabelle/HOL. A proof assistant for higher-order logic
• Mizar: state-of-the-art and beyond
• Partizan Games in Isabelle/HOLZF
• The Isabelle Framework
• The ring of Conway numbers in Mizar
• The role of the Mizar mathematical library for interactive proof development in Mizar
• Types for Proofs and Programs

Cited in

(1)

• Surreal numbers: a study of square roots

This page was built for publication: Inverse element for surreal number

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6966341)