Module

Algebra_norm_of_subsingleton.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_norm_of_subsingleton

1 declaration indexed from sourceView source ↗

Module documentation

Imports1

Imported by2

theorem

Algebra.norm_of_subsingleton

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_norm_of_subsingleton

Lean source · statement

theorem _root_.Algebra.norm_of_subsingleton {R A : Type*} [CommRing R] [Ring A] [Algebra R A]
  [Subsingleton A] (a : A) : Algebra.norm R a = 1