Trivial

📁 Source: Mathlib/RingTheory/Valuation/ValuativeRel/Trivial.lean

Statistics

Metric	Count
Definitions Trivial, trivialRel	2
Theorems eq_trivialRel_of_compatible_one, isDiscrete_trivialRel, not_isNontrivial_of_trivialRel, subsingleton_units_valueGroupWithZero_of_trivialRel, trivialRel_eq_ofValuation_one	5
Total	7

Bundle

Definitions

Name	Category	Theorems
Trivial 📖	CompOp	24 math math: Trivial.continuousLinearEquivAt_trivialization, Trivial.symmL_trivialization, Trivial.continuousLinearMapAt_trivialization, Trivial.fiberBundle_trivializationAtlas', instIsContinuousRiemannianBundleTrivial, Trivial.vectorBundle, Trivial.trivialization_target, Trivial.linearMapAt_trivialization, Trivial.trivialization_symm_apply, Trivial.homeomorphProd_symm_apply_snd, Trivial.trivialization_apply, Trivial.trivialization.isLinear, Trivial.toOpenPartialHomeomorph_trivialization_symm_apply, Trivial.homeomorphProd_symm_apply_proj, instIsContMDiffRiemannianBundleTrivial, Trivial.fiberBundle_trivializationAt', Trivial.contMDiffVectorBundle, Trivial.trivialization.coordChangeL, Trivial.symmₗ_trivialization, Trivial.trivialization_baseSet, Trivial.trivialization_symm_apply_proj, Trivial.homeomorphProd_apply, Trivial.trivialization_source, Trivial.trivialization_symm_apply_snd

ValuativeRel

Definitions

Name	Category	Theorems
trivialRel 📖	CompOp	2 math math: eq_trivialRel_of_compatible_one, trivialRel_eq_ofValuation_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_trivialRel_of_compatible_one 📖	mathematical	—	trivialRel	—	IsDomain.toNontrivial IsDomain.to_noZeroDivisors ext Valuation.Compatible.vle_iff_le map_zero MonoidWithZeroHomClass.toZeroHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass GroupWithZero.toNontrivial Valuation.one_apply_of_ne_zero
isDiscrete_trivialRel 📖	mathematical	—	IsDiscrete	—	IsDomain.toNontrivial IsDomain.to_noZeroDivisors zero_lt_one LinearOrderedCommMonoidWithZero.toZeroLeOneClass NeZero.one GroupWithZero.toNontrivial subsingleton_units_valueGroupWithZero_of_trivialRel GroupWithZero.eq_zero_or_unit Units.val_one Units.val_lt_val
not_isNontrivial_of_trivialRel 📖	mathematical	—	IsNontrivial	—	IsDomain.toNontrivial IsDomain.to_noZeroDivisors subsingleton_units_valueGroupWithZero_of_trivialRel GroupWithZero.eq_zero_or_unit
subsingleton_units_valueGroupWithZero_of_trivialRel 📖	mathematical	—	Units ValueGroupWithZero MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero instLinearOrderedCommGroupWithZeroValueGroupWithZero	—	IsDomain.toNontrivial IsDomain.to_noZeroDivisors isEquiv instCompatibleValueGroupWithZeroValuation exists_valuation_posSubmonoid_div_valuation_posSubmonoid_eq Units.ext_iff div_eq_div_iff map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass Valuation.IsEquiv.val_eq one_apply_posSubmonoid mul_one
trivialRel_eq_ofValuation_one 📖	mathematical	—	trivialRel ofValuation Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero CommRing.toRing Valuation.one IsDomain.toNontrivial CommSemiring.toSemiring CommRing.toCommSemiring IsDomain.to_noZeroDivisors MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	IsDomain.toNontrivial IsDomain.to_noZeroDivisors eq_trivialRel_of_compatible_one Valuation.Compatible.ofValuation

---

← Back to Index