TheoremsofValuation, srel_iff_lt, vle_iff_le, apply_posSubmonoid_ne_zero, apply_posSubmonoid_pos, one_rel_iff, one_srel_iff, one_vle_iff, one_vlt_iff, rel_iff_le, rel_one_iff, srel_iff_lt, srel_one_iff, veq_iff_eq, vle_iff_le, vle_one_iff, vlt_iff_lt, vlt_one_iff, compatible_comap, mapPosSubmonoid_apply_coe, mapValueGroupWithZero_mk, mapValueGroupWithZero_strictMono, mapValueGroupWithZero_valuation, srel_iff_srel, vle_iff_vle, vlt_iff_vlt, vle_iff_le, has_maximal_element, condition, exists_lt_one, nonempty, of_valuativeExtension, strictMono, refl, rfl, trans, trans', trans_srel, rel, trans, trans_rel, bot_eq_zero, embed_mk, embed_strictMono, embed_valuation_eq_restrict₀, embedding_embed_valuation_eq, embedding_orderMonoidIso_valuation_eq, exact, ind, inv_mk, leftInverse_embedding_orderMonoidIso, lift_mk, lift_mul, lift_one, lift_valuation, lift_zero, lift₂_mk, mk_eq_div, mk_eq_mk, mk_eq_one, mk_eq_valuation, mk_eq_zero, mk_le_mk, mk_lt_mk, mk_mul_mk, mk_one_one, mk_pos, mk_self, mk_zero, orderMonoidIso_embed, orderMonoidIso_mk, orderMonoidIso_strictMono, orderMonoidIso_valuation_eq_restrict₀, sound, div_rel_iff, div_rel_one_iff, div_vle_iff, div_vle_one_iff, exists_valuation_div_valuation_eq, exists_valuation_posSubmonoid_div_valuation_posSubmonoid_eq, ext, ext_iff, instCompatibleValueGroupWithZeroValuation, instIsNontrivialOfIsNontrivialOfCompatible, instIsOrderedMonoidValueGroupWithZero, instIsPrimeSupp, instMulArchimedeanValueGroupWithZeroOfIsRankLeOne, instReflVeq, instReflVle, instSymmVeq, instValuativePreorderWithPreorder, inv_rel_one, inv_srel_one, inv_vle_one, inv_vlt_one, isEquiv, isNontrivial_iff_isNontrivial, isNontrivial_iff_nontrivial_units, le_uniformizer_iff, left_cancel_posSubmonoid, mul_rel_mul, mul_rel_mul_iff_left, mul_rel_mul_iff_right, mul_srel_mul, mul_srel_mul_iff_left, mul_srel_mul_iff_right, mul_srel_mul_of_rel_of_srel, mul_srel_mul_of_srel_of_rel, mul_veq_mul, mul_vle_mul, mul_vle_mul_iff_left, mul_vle_mul_iff_right, mul_vle_mul_left, mul_vle_mul_right, mul_vlt_mul, mul_vlt_mul_iff_left, mul_vlt_mul_iff_right, mul_vlt_mul_left, mul_vlt_mul_of_vle_of_vlt, mul_vlt_mul_of_vlt_of_vle, mul_vlt_mul_right, not_rel_one_zero, not_srel_iff, not_vgt_of_veq, not_vle, not_vle_one_zero, not_vlt, not_vlt_of_veq, not_vlt_zero, one_apply_posSubmonoid, one_rel_div_iff, one_rel_inv, one_srel_inv, one_vle_div_iff, one_vle_inv, one_vlt_inv, posSubmonoid_def, pow_rel_pow, pow_rel_pow_of_one_rel, pow_rel_pow_of_rel_one, pow_srel_pow, pow_vle_pow, pow_vle_pow_of_one_vle, pow_vle_pow_of_vle_one, pow_vlt_pow, rel_add, rel_add_cases, rel_div_iff, rel_mul, rel_mul_cancel, rel_mul_left, rel_mul_left_iff, rel_mul_right, rel_mul_right_iff, rel_refl, rel_rfl, rel_total, rel_trans, rel_trans', rel_zero_iff, restrict_lt_orderMonoidIso, right_cancel_posSubmonoid, srel_iff, srel_mul_left, srel_mul_left_iff, srel_mul_right, srel_mul_right_iff, srel_of_rel_of_srel, srel_of_srel_of_rel, supp_def, supp_eq_valuation_supp, uniformizer_inv_le_iff, uniformizer_lt_one, uniformizer_ne_zero, uniformizer_pos, val_posSubmonoid_ne_zero, valuation_eq_zero_iff, valuation_lt_symm_orderMonoidIso, valuation_posSubmonoid_ne_zero, valuation_surjective, not_vgt, not_vlt, refl, rfl, vge, vle, veq_comm, veq_def, veq_refl, veq_rfl, veq_trans, veq_zero_iff, vge_of_veq, not_vlt, refl, rfl, trans, trans', trans_vlt, vle_add, vle_add_cases, vle_div_iff, vle_mul_cancel, vle_mul_left_iff, vle_mul_right, vle_mul_right_iff, vle_of_veq, vle_refl, vle_rfl, vle_total, vle_trans, vle_trans', vle_zero_iff, ne_zero, not_vle, trans, trans_vle, vle, vlt_mul_left, vlt_mul_left_iff, vlt_mul_right, vlt_mul_right_iff, vlt_of_vle_of_vlt, vlt_of_vlt_of_vle, zero_rel, zero_srel_coe_posSubmonoid, zero_srel_iff, zero_srel_mul, zero_srel_one, zero_veq_iff, zero_vle, zero_vlt_coe_posSubmonoid, zero_vlt_iff, zero_vlt_mul, zero_vlt_one | 235 |