Theorems · Inductive type · commutative algebra

Valuation.IsTrivialOn

{Γ₀ : Type u_4} →
  [inst : LinearOrderedCommMonoidWithZero Γ₀] →
    {B : Type u_7} →
      (A : Type u_8) → [inst_1 : CommSemiring A] → [inst_2 : Ring B] → [Algebra A B] → Valuation B Γ₀ → Prop

A valuation on an A-algebra B is trivial on constants if the nonzero elements of the base ring A are mapped to 1. This is true, for example, when A is a finite field. See Valuation.FiniteField.instIsTrivialOn.

Defined in

Mathlib.RingTheory.Valuation.Basic

Cited by

28 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

LinearOrderedCommMonoidWithZeroCommSemiringRingAlgebra